theorem
L26 ↗evalFun_mul
AlgebraicCurve.Divisor.evalFun_mul
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_evalFun_mul
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Divisor.evalFun_mul {K F : Type*} [Field K] [Field F] [Algebra K
F] {f g : F} {D : Divisor K F} (hrat : ∀ v ∈ D.support, Place.IsRational v) (hf : ∀ v ∈
D.support, f ∈ v.toValuationSubring) (hg : ∀ v ∈ D.support, g ∈ v.toValuationSubring) :
Divisor.evalFun (f * g) D = Divisor.evalFun f D * Divisor.evalFun g D