Commit 2024-10-28 15:32 04cd6e34

View on Github →

feat(RingTheory/Flat): faithfully flat ring maps (#15014) Add definition of faithfully flat ring maps and show basic properties. This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.

Estimated changes

Modified Mathlib/RingTheory/Flat/FaithfullyFlat.lean

added theorem Module.FaithfullyFlat.comp

added theorem Module.FaithfullyFlat.iff_zero_iff_lTensor_zero

added theorem Module.FaithfullyFlat.iff_zero_iff_rTensor_zero

added theorem Module.FaithfullyFlat.of_linearEquiv

added theorem Module.FaithfullyFlat.zero_iff_lTensor_zero

added theorem Module.FaithfullyFlat.zero_iff_rTensor_zero