21.1. Keystones🔗

TailSpace — source · report an issue

abbrev TailSpace (X : Type*) : Type _

riemannRoch_tailForm — source · report an issue

theorem riemannRoch_tailForm (D : Divisor X) :
    (lDim (X := X) D : ℤ) - h1TailDim (X := X) D
      = Divisor.deg X D + 1 - h1TailDim (X := X) 0