AlgebraicCurve.mul_mem_lSpace_nsmul_succ_and_reflects_of_poleDivisor
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceNsmulSuccReflects
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.mul_mem_lSpace_nsmul_succ_and_reflects_of_poleDivisor
{K F : Type*} [Field K] [Field F] [Algebra K F]
(x : F) (D : Divisor K F) (hD : ∀ v : Place K F, D v = max 0 (-v.ord x))
(m : ℕ) :
(∀ g ∈ LSpace ((m : ℕ) • D), x * g ∈ LSpace ((m + 1) • D)) ∧
(∀ g ∈ LSpace ((m + 1) • D), x * g ∈ LSpace ((m + 1) • D) → g ∈ LSpace (m • D))