Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-07-13 20:05
79741dbd
View on Github →
feat(RingTheory/Flat): a module is flat iff tensoring preserves exact sequences (
#14482
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/RingTheory/Flat/CategoryTheory.lean
added
theorem
Module.Flat.iff_lTensor_preserves_shortComplex_exact
added
theorem
Module.Flat.iff_rTensor_preserves_shortComplex_exact
added
theorem
Module.Flat.lTensor_shortComplex_exact
added
theorem
Module.Flat.rTensor_shortComplex_exact