theorem
L27 ↗pushforward_div
AlgebraicCurve.Divisor.pushforward_div
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforward_div
open AlgebraicCurve AlgebraicCurve.DivisorLean source · statement
theorem _root_.AlgebraicCurve.Divisor.pushforward_div {K F F' : Type*} [Field K] [Field F] [Field
F'] [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F'] [FiniteDimensional F F']
[Algebra.IsSeparable F F'] [CharZero F] [HasPrincipalDivisors K F'] {f : F'} (hf : f ≠ 0) {D :
Divisor K F'} (hD : ∀ w, D w = w.ord f) {E : Divisor K F} (hE : ∀ v, E v = v.ord (Algebra.norm F
f)) : Divisor.pushforward F D = E