Commit 2025-08-15 15:34 5a5a2847

View on Github →

feat(RingTheory): faithfully flat ring maps (#24530) Co-authored by: Joël Riou rioujoel@gmail.com

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Ring/Equiv.lean

added theorem RingEquiv.comp_ofBijective_symm

added theorem RingEquiv.ofBijective_symm_comp

Created Mathlib/RingTheory/RingHom/FaithfullyFlat.lean

added theorem RingHom.FaithfullyFlat.eq_and

added theorem RingHom.FaithfullyFlat.flat

added theorem RingHom.FaithfullyFlat.iff_flat_and_comap_surjective

added theorem RingHom.FaithfullyFlat.isStableUnderBaseChange

added theorem RingHom.FaithfullyFlat.of_bijective

added theorem RingHom.FaithfullyFlat.respectsIso

added theorem RingHom.FaithfullyFlat.stableUnderComposition

added def RingHom.FaithfullyFlat

added theorem RingHom.faithfullyFlat_algebraMap_iff

Modified Mathlib/RingTheory/RingHom/Flat.lean

added theorem RingHom.flat_algebraMap_iff

deleted theorem flat_algebraMap_iff