Theorem RingHom.FormallySmooth.of_flat_of_ker_eq_map_of_square_zero

Modification history

2026-04-08 16:40
Mathlib/RingTheory/Smooth/Quotient.lean
feat(RingTheory/Smooth): some lemmas about formally smooth (#35675) …
Added RingHom.FormallySmooth.of_flat_of_ker_eq_map_of_square_zeroView on Github →