AlgebraicCurve.CurveModel.ord_placeOfPoint_ffEquiv_symm_germToFunctionField_eq_zero_of_isUnit
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurve.CurveModel
open _root_.AlgebraicCurves.Models.Proofs in
open CurveModel_ord_placeOfPoint_ffEquiv_symm_germToFunctionField_eq_zero_of_isUnit in
open CategoryTheory AlgebraicGeometry AlgebraicCurve inLean source · statement
theorem ord_placeOfPoint_ffEquiv_symm_germToFunctionField_eq_zero_of_isUnit
{K : Type} [Field K] {L : Type} [Field L] [Algebra K L] (Mc : AlgebraicCurve.CurveModel K L)
(U : Mc.C.Opens) (P : closedPoints Mc.C) (hP : P.1 ∈ U)
[Nonempty (Scheme.Opens.toScheme U)] (s : Γ(Mc.C, U)) (hs : IsUnit s) :
(Mc.placeOfPoint P).ord (Mc.ffEquiv.symm (Mc.C.germToFunctionField U s)) = 0