theorem Lemma2112.ell_eq_one_iff_principal {C : Type u_1} {F : Type u_2} {k : Type u_3} [Field k] [Field F] [Algebra k F] [RiemannRochData C F k] (D : CurveDivisor C) (hdeg : (CurveDivisor.degree C) D = 0) : RiemannRochSpace.divisorDim D = 1 ↔ CurveWithOrd.IsPrincipal D

(Lemma 21.12) A divisor $D$ of degree $0$ has $\ell(D) = 1$ iff $D$ is principal.