Module

FiniteDimensional_lSpace_zero.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.FiniteDimensional_lSpace_zero

1 declaration indexed from sourceView source ↗

Module documentation

Finite Dimensional l Space zero

Imports2

Imported by5

theorem

finiteDimensional_lSpace_zero

AlgebraicCurve.finiteDimensional_lSpace_zero

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FiniteDimensional_lSpace_zero
noncomputable section
universe u v
open AlgebraicCurve

Lean source · statement

theorem _root_.AlgebraicCurve.finiteDimensional_lSpace_zero
    (K : Type u) (F : Type v) [Field K] [Field F] [Algebra K F]
    [IsCurveOver K F] [Algebra.EssFiniteType K F] [Nonempty (Place K F)] :
    FiniteDimensional K (LSpace (0 : Divisor K F))