AlgebraicCurve.degree_canonicalDivisor_eq_of_riemannRoch
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.Degree_canonicalDivisor_eq_of_riemannRoch
open AlgebraicCurve KaehlerDifferentialLean source · statement
theorem _root_.AlgebraicCurve.degree_canonicalDivisor_eq_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) :
Divisor.degree (canonicalDivisorOf hω) = 2 * (genus K F : ℤ) - 2