AlgebraicCurve.Divisor.evalFun_single_sub_single
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_evalFun_single_sub_single
open AlgebraicCurve AlgebraicCurve.DivisorLean source · statement
theorem _root_.AlgebraicCurve.Divisor.evalFun_single_sub_single {K F : Type*} [Field K] [Field
F] [Algebra K F] (f : F) {v₁ v₂ : Place K F} (h₁ : v₁.evalAt f ≠ 0) (h₂ : v₂.evalAt f ≠ 0) :
Divisor.evalFun f (Finsupp.single v₁ 1 + Finsupp.single v₂ (-1)) = v₁.evalAt f / v₂.evalAt
f