AlgebraicCurve.Divisor.pushforward_div_of_isSeparable
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforward_div_of_isSeparable
open AlgebraicCurve AlgebraicCurve.DivisorLean source · statement
theorem _root_.AlgebraicCurve.Divisor.pushforward_div_of_isSeparable {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'] [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