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}