AlgebraicCurve.Place.eq_ord_of_addHom_of_nonneg_iff
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_eq_ord_of_addHom_of_nonneg_iff
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Place.eq_ord_of_addHom_of_nonneg_iff {K F : Type*} [Field K] [Field
F] [Algebra K F] (w : Place K F) (φ : F → ℤ)
(hmul : ∀ x y, x ≠ 0 → y ≠ 0 → φ (x * y) = φ x + φ y)
(hone : ∃ t, t ≠ 0 ∧ φ t = 1)
(hiff : ∀ x, x ≠ 0 → (0 ≤ φ x ↔ x ∈ w.toValuationSubring))
{x : F} (hx : x ≠ 0) : φ x = w.ord x