Theorem Algebra.FormallySmooth.of_surjective_of_ker_eq_map_of_flat

Modification history

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