A chosen uniformizer in each place valuation ring and its order and nonvanishing properties.
A chosen irreducible element of the valuation ring, viewed in the function field.
Surrounding namespaces, section variables, and local commands at this declaration.
open KaehlerDifferential
noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)def uniformizer : FSurrounding namespaces, section variables, and local commands at this declaration.
open KaehlerDifferential
noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)theorem ord_uniformizer : v.ord v.uniformizer = 1Surrounding namespaces, section variables, and local commands at this declaration.
open KaehlerDifferential
noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)theorem uniformizer_ne_zero : v.uniformizer ≠ 0Surrounding namespaces, section variables, and local commands at this declaration.
open KaehlerDifferential
noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)theorem dCoord_eq : v.dCoord = KaehlerDifferential.D K F v.uniformizer