AlgebraicCurve.Place.ord_eq_zero_of_isIntegral_adjoin
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_eq_zero_of_isIntegral_adjoin
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Place.ord_eq_zero_of_isIntegral_adjoin {K F : Type*} [Field K] [Field
F] [Algebra K F] (v : Place K F) {j x : F} (hj : j ∈ v.toValuationSubring) (hx : IsIntegral
(Algebra.adjoin K {j}) x) (hx' : IsIntegral (Algebra.adjoin K {j}) x⁻¹) : v.ord x = 0