Theorem RingHom.FaithfullyFlat.iff_flat_and_comap_surjective

Modification history

2025-08-15 15:34
Mathlib/RingTheory/RingHom/FaithfullyFlat.lean
feat(RingTheory): faithfully flat ring maps (#24530) …
Added RingHom.FaithfullyFlat.iff_flat_and_comap_surjectiveView on Github →