Theorem derivationQuotKerSq_mk

feat(RingTheory/Smooth): formally smooth iff `H¹(L_{R/S}) = 0` and `Ω_{S/R}` is projective (#17905)