finrank_CotangentSpace_eq_one — Mathlib

English

If R is a domain and a discrete valuation ring, then finrank of the cotangent space equals 1.

Русский

Если R — домен и дискретное оценочное кольцо, то размерность cotangent пространства равна 1.

LaTeX

$$finrank(ResidueField(R))(CotangentSpace(R)) = 1$$

Lean4

theorem finrank_CotangentSpace_eq_one [IsDomain R] [IsDiscreteValuationRing R] :
    finrank (ResidueField R) (CotangentSpace R) = 1 :=
  finrank_CotangentSpace_eq_one_iff.mpr ‹_›

Похожие утверждения