theorem cotangentSpace_dim_ge_krullDim (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] : ringKrullDim R ≤ ↑(Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R))

Lemma 30 (Lecture 18): For a Noetherian local ring R, the Krull dimension is bounded above by the residue-field dimension of the Zariski cotangent space, i.e. dim R ≤ dim T*_x X.