theorem
L23 ↗exists_ord_eq_one
AlgebraicCurve.Place.exists_ord_eq_one
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_ord_eq_oneLean source · statement
theorem _root_.AlgebraicCurve.Place.exists_ord_eq_one {K F : Type*} [Field K] [Field F] [Algebra K
F] (v : AlgebraicCurve.Place K F) :
∃ t : F, v.ord t = 1