AlgebraicCurve.Place.ord_eq_zero_of_evalAt_ne_zero
Nonzero evaluation at a rational place detects an actual unit in its valuation ring, and hence a function of order zero.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace AlgebraicCurve.PlaceLean source · statement
theorem ord_eq_zero_of_evalAt_ne_zero
{K F : Type*} [Field K] [Field F] [Algebra K F]
(v : Place K F) (hv : v.IsRational) {f : F}
(h : v.evalAt f ≠ 0) : v.ord f = 0