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