Commit 2025-01-07 20:32 1c56cac6

View on Github →

feat(RingTheory): Jacobian criterion for smoothness of local algebras (#20326)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/Smooth/Kaehler.lean

added theorem Algebra.Extension.formallySmooth_iff_split_injection

Created Mathlib/RingTheory/Smooth/Local.lean

added theorem Algebra.FormallySmooth.iff_injective_lTensor_residueField