theorem
L30 ↗evalAt_inv
AlgebraicCurve.Place.evalAt_inv
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_inv
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Place.evalAt_inv {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⁻¹ =
(v.evalAt f)⁻¹