Theorem Algebra.Extension.cotangentComplexBaseChange_eq_lTensor_cotangentComplex

Modification history

2025-12-15 10:15
Mathlib/RingTheory/Extension/Cotangent/Basic.lean
feat(RingTheory): more ergonomic version of jacobi criterion for smoothness (#32802)
Added Algebra.Extension.cotangentComplexBaseChange_eq_lTensor_cotangentComplexView on Github →