The Riemann–Roch theorem

This is pure packaging of the duality theorem together with the definition of the index of specialty.

theorem FunctionField.Chart.riemann_roch (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] {W : DivisorA k K} (hW : IsCanonical k K W) (D : DivisorA k K) : ↑(ell k K D) = deg k K D + 1 - ↑(genus k K) + ↑(ell k K (W - D))

Riemann–Roch (Stichtenoth Thm. 1.5.15): for a canonical divisor W,

ℓ(D) = deg D + 1 − g + ℓ(W − D).