theorem weilDifferentials_dim_eq_indexOfSpeciality {F : Type u_1} [Field F] {P : Type u_2} [DecidableEq P] {O : P → ValuationSubring F} (k : Type u_3) [Field k] [Algebra k F] [FunctionFieldAdeleRing.ConstantField k] [FunctionFieldAdeleRing.FunctionFieldProperty F P O] [FunctionFieldAdeleRing.DiscreteValuationFamily P F k] [HasResidueFieldSurjection P F k O] (D : P →₀ ℤ) : ↑(Module.finrank k ↥(FunctionFieldAdeleRing.weilDifferentials k ⇑D)) = adeleIndexOfSpeciality k D

Lemma 22.13. The $k$-dimension of the Weil differentials regular at the divisor $D$ equals the index of speciality: $\dim_k \Omega(D) = i(D)$.