theorem
L25 ↗evalFun_add
AlgebraicCurve.Divisor.evalFun_add
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_evalFun_add
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Divisor.evalFun_add {K F : Type*} [Field K] [Field F] [Algebra K
F] (f : F) {D E : Divisor K F} (hD : ∀ v ∈ D.support, Place.evalAt v f ≠ 0) (hE : ∀ v ∈
E.support, Place.evalAt v f ≠ 0) : Divisor.evalFun f (D + E) = Divisor.evalFun f D *
Divisor.evalFun f E