Commit 2024-07-05 09:16 e7abe8ca

View on Github →

feat(RingTheory/Flat/Basic): a module is flat iff tensoring is left exact (non-categorical formulation) (#14234) This is stated in terms of Function.Exact

Estimated changes

Modified Mathlib/Algebra/Exact.lean

added theorem Function.Exact.comp_injective

Modified Mathlib/RingTheory/Flat/Basic.lean

added theorem Module.Flat.iff_lTensor_exact

added theorem Module.Flat.iff_rTensor_exact

added theorem Module.Flat.lTensor_exact

added theorem Module.Flat.rTensor_exact