Differential properties of formally unramified algebras

We show that R-algebra A is formally unramified iff the Kaehler differentials vanish.

instance Algebra.FormallyUnramified.subsingleton_kaehlerDifferential {R : Type u} {S : Type u} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FormallyUnramified R S] : Subsingleton (Ω[S⁄R])

Equations

• ⋯ = ⋯

theorem Algebra.FormallyUnramified.iff_subsingleton_kaehlerDifferential {R : Type u} {S : Type u} [CommRing R] [CommRing S] [Algebra R S] : Algebra.FormallyUnramified R S ↔ Subsingleton (Ω[S⁄R])