theorem isRegularLocalRing_iff_free_kaehlerDifferential (k : Type u_1) (R : Type u_2) [Field k] [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Algebra k R] : IsRegularLocalRing R ↔ Module.Free R Ω[R⁄k]

Smoothness via Kähler differentials: a Noetherian local k-algebra R is a regular local ring iff Ω_{R/k} is R-free. Geometrically, "smooth ⇔ Ω is locally free of the expected rank".

theorem remark28_completed_local_ring_iso_power_series (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (hreg : IsRegularLocalRing R) (n : ℕ) (hdim : ringKrullDim R = ↑n) : Nonempty (AdicCompletion (IsLocalRing.maximalIdeal R) R ≃+* MvPowerSeries (Fin n) (IsLocalRing.ResidueField R))

Remark 28 (Cohen's structure theorem, complete regular local case): the 𝔪-adic completion of an n-dimensional regular local ring R is isomorphic to the formal power series ring κ[[x₁, …, xₙ]] over its residue field κ.