theorem
L26 ↗evalFun_zpow_left
AlgebraicCurve.Divisor.evalFun_zpow_left
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_evalFun_zpow_left
open AlgebraicCurve AlgebraicCurve.DivisorLean source · statement
theorem _root_.AlgebraicCurve.Divisor.evalFun_zpow_left {K F : Type*} [Field K] [Field F]
[Algebra K F] {f : F} (hf : f ≠ 0) {D : Divisor K F} (n : ℤ) (hrat : ∀ v ∈ D.support,
Place.IsRational v) (hord : ∀ v ∈ D.support, Place.ord v f = 0) : Divisor.evalFun (f ^ n)
D = Divisor.evalFun f D ^ n