Commit 2026-04-08 16:40 461ef7d2

View on Github →

feat(RingTheory/Smooth): some lemmas about formally smooth (#35675) This PR mainly formalized the result [Stacks 031L] This is a preliminary of Cohen Structure Theorem.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/Ideal/Cotangent.lean

added theorem Ideal.mapCotangent_ker_of_surjective

added theorem Ideal.mapCotangent_surjective_of_comap_eq

Modified Mathlib/RingTheory/Ideal/Maps.lean

added theorem Ideal.eq_map_of_comap_eq_ker_sup

added theorem Ideal.exists_of_comap_eq_ker_sup

Created Mathlib/RingTheory/Smooth/Quotient.lean

added theorem Algebra.FormallySmooth.of_surjective_of_ker_eq_map_of_flat

added theorem LinearMap.ker_inf_smul_top_eq_smul_of_flat

added theorem RingHom.FormallySmooth.of_flat_of_ker_eq_map_of_square_zero

Modified Mathlib/RingTheory/TensorProduct/Quotient.lean

added theorem Ideal.subtype_rTensor_range