Theorem RingHom.FaithfullyFlat.injective

Modification history

2025-09-27 16:22
Mathlib/RingTheory/RingHom/FaithfullyFlat.lean
feat(Mathlib/AlgebraicGeometry/Morphisms/Flat): add simple properties of flat maps (#30021) …
Added RingHom.FaithfullyFlat.injectiveView on Github →