Mathlib Changelog
v4
Changelog
About
Github
Theorem
Module.Flat.iff_rTensor_injective
Modification history
2023-10-31 10:54
Mathlib/RingTheory/Flat.lean
feat(RingTheory/Flat): free and projective modules over a `CommRing` are flat (#7567) …
Added
Module.Flat.iff_rTensor_injective
View on Github →