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