Module

Exists_riemannGenusReachedAt_nsmul_single_of_stichtenothGenusExists.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_riemannGenusReachedAt_nsmul_single_of_stichtenothGenusExists

1 declaration indexed from sourceView source ↗

Module documentation

Exists riemann Genus Reached At nsmul single of stichtenoth Genus Exists

Imports7

Imported by3

theorem

exists_riemannGenusReachedAt_nsmul_single_of_stichtenothGenusExists

L32 ↗

AlgebraicCurve.exists_riemannGenusReachedAt_nsmul_single_of_stichtenothGenusExists

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsGenusReachedNsmulSingle
open AlgebraicCurve

Lean source · statement

theorem _root_.AlgebraicCurve.exists_riemannGenusReachedAt_nsmul_single_of_stichtenothGenusExists
    {K F : Type*} [Field K] [Field F] [Algebra K F] [IsCurveOver K F]
    [Nonempty (Place K F)] [FiniteDimensional K ↥(LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) (Q : Place K F) :
    ∃ n : ℕ, RiemannGenusReachedAt γ ((n : ℤ) • Finsupp.single Q 1)

Module documentation

Exists riemann Genus Reached At nsmul single of stichtenoth Genus Exists

Declarations

exists_riemannGenusReachedAt_nsmul_single_of_stichtenothGenusExists