Theorem Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange_residueField

Modification history

2025-12-15 10:15
Mathlib/RingTheory/Smooth/Local.lean
feat(RingTheory): more ergonomic version of jacobi criterion for smoothness (#32802)
Added Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange_residueFieldView on Github →