AlgebraicCurve.ell_canonicalDivisor_eq_genus_of_riemannRoch
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.Ell_canonicalDivisor_eq_genus_of_riemannRoch
open AlgebraicCurve KaehlerDifferentialLean source · statement
theorem _root_.AlgebraicCurve.ell_canonicalDivisor_eq_genus_of_riemannRoch {K F : Type*} [Field K]
[Field F] [Algebra K F] [IsCurveOver K F] [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K
F, v.DCoordGenerates] (hRR : FunctionFieldRiemannRoch K F) (hC : ConstantsAreBase K F) {ω :
Ω[F⁄K]} (hω : ω ≠ 0) :
(ell (canonicalDivisorOf hω) : ℤ) = (genus K F : ℤ)