Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-12-15 10:15
55531ff0
View on Github →
feat(RingTheory): more ergonomic version of jacobi criterion for smoothness (
#32802
)
Estimated changes
Modified
Mathlib/RingTheory/Extension/Basic.lean
added
theorem
Algebra.Extension.contangentEquiv_tmul
Modified
Mathlib/RingTheory/Extension/Cotangent/Basic.lean
added
theorem
Algebra.Extension.cotangentComplexBaseChange_eq_lTensor_cotangentComplex
added
theorem
Algebra.Extension.lTensor_cotangentComplex_eq_cotangentComplexBaseChange
added
def
KaehlerDifferential.cotangentComplexBaseChange
added
theorem
KaehlerDifferential.cotangentComplexBaseChange_tmul
Modified
Mathlib/RingTheory/Smooth/Local.lean
added
theorem
Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange
added
theorem
Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange_residueField
modified
theorem
Algebra.FormallySmooth.iff_injective_lTensor_residueField.{u}