Mathlib Changelog
v4
Changelog
About
Github
Theorem
derivationQuotKerSq_mk
Modification history
2024-11-02 12:25
Mathlib/RingTheory/Smooth/Kaehler.lean
feat(RingTheory/Smooth): formally smooth iff `H¹(L_{R/S}) = 0` and `Ω_{S/R}` is projective (#17905)
Added
derivationQuotKerSq_mk
View on Github →