Commit 2023-10-31 10:54 cddb28fc
View on Github →feat(RingTheory/Flat): free and projective modules over a CommRing are flat (#7567)
Prove that flat modules are stable under retracts, isomorphisms and direct sums. Use this to deduce that free and projective modules are flat.