theorem
L29 ↗evalAt_ne_zero
AlgebraicCurve.Place.evalAt_ne_zero
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_ne_zero
open IsLocalRing AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Place.evalAt_ne_zero {K F : Type*} [Field K] [Field F]
[Algebra K F] (v : Place K F) (hv : v.IsRational) {f : F} (hf : f ≠ 0) (h : v.ord f = 0) :
v.evalAt f ≠ 0