Commit 2024-10-16 15:54 8d6f380f

View on Github →

feat(RingTheory/Flat/Basic): drop [Small.{v} R] assumption in Module.Flat.iff_* lemmas (#17484) Drop [Small.{v} R] assumption from Module.Flat.iff_* lemmas Module.Flat.iff_rTensor_preserves_injective_linearMap, Module.Flat.iff_lTensor_exact, and so on.

Estimated changes

Modified Mathlib/RingTheory/Flat/Basic.lean

added theorem Module.Flat.equiv_iff

added theorem Module.Flat.iff_lTensor_exact'

modified theorem Module.Flat.iff_lTensor_exact

added theorem Module.Flat.iff_lTensor_preserves_injective_linearMap'

modified theorem Module.Flat.iff_lTensor_preserves_injective_linearMap

added theorem Module.Flat.iff_rTensor_exact'

modified theorem Module.Flat.iff_rTensor_exact

added theorem Module.Flat.iff_rTensor_preserves_injective_linearMap'

modified theorem Module.Flat.iff_rTensor_preserves_injective_linearMap

modified theorem Module.Flat.lTensor_exact

modified theorem Module.Flat.rTensor_exact