theorem
L25 ↗exists_of_orderMap
AlgebraicCurve.Place.exists_of_orderMap
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_orderMap
open WithZeroLean source · statement
theorem _root_.AlgebraicCurve.Place.exists_of_orderMap {K F : Type*} [Field K] [Field F] [Algebra K
F]
(μ : F → WithTop ℤ) (h_top : ∀ x, μ x = ⊤ ↔ x = 0)
(h_mul : ∀ x y, μ (x * y) = μ x + μ y) (h_add : ∀ x y, min (μ x) (μ y) ≤ μ (x + y))
(h_const : ∀ c : K, c ≠ 0 → μ (algebraMap K F c) = 0) (h_nontriv : ∃ x, 0 < μ x ∧ μ x ≠ ⊤) :
∃ (P : AlgebraicCurve.Place K F) (e : ℕ), 0 < e ∧
(∀ x, x ∈ P.toValuationSubring ↔ 0 ≤ μ x) ∧
∀ x, x ≠ 0 → μ x = (((e : ℤ) * P.ord x : ℤ) : WithTop ℤ)