AlgebraicCurve.Divisor.pushforwardAlong_single_one
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardAlong_single_one
open AlgebraicCurve inLean source · statement
theorem _root_.AlgebraicCurve.Divisor.pushforwardAlong_single_one
{K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
(ψ : F →ₐ[K] F') (hψ : ψ.toRingHom.IsIntegral) (W : AlgebraicCurve.Place K F')
(hW : W.deg = 1) (hV : (W.restrictAlong ψ hψ).deg = 1) :
AlgebraicCurve.Divisor.pushforwardAlong ψ hψ (Finsupp.single W 1) =
Finsupp.single (W.restrictAlong ψ hψ) 1