Places Over Finite
Abstract
An absolute value above a finite place is a positive power of a finite place upstairs.
Theorem 1.1 (Places Over Finite).
Lean statement: D5/S3/Arith/DiophantineApproximation/PlacesOverFinite.exists_finitePlace_rpow_inv_eq_of_liesOver
Proof. Machine-checked in Lean as D5/S3/Arith/DiophantineApproximation/PlacesOverFinite.exists_finitePlace_rpow_inv_eq_of_liesOver (✓ std3). ∎
Citation. Ralf Stephan (2026). Subspace-Theorems. URL: https://github.com/rwst/Subspace-Theorems/tree/bfd830f481b296989fa5f0c1e48d9316f72270d8.
Commentary.
An absolute value above a finite place is a positive power of a finite place upstairs.