Commit 2025-09-15 21:27 4c5068bf

View on Github →

feat(RingTheory/Flat): Add theorems relating Submodule.torsion and Module.Flat (#26783)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Bilinear.lean

added theorem LinearMap.lift_lsmul_mul_eq_lsmul_lift_lsmul

Modified Mathlib/Algebra/Module/LocalizedModule/Basic.lean

added theorem IsLocalizedModule.noZeroSMulDivisors

Created Mathlib/RingTheory/Flat/TorsionFree.lean

added theorem IsDedekindDomain.flat_iff_torsion_eq_bot

added theorem Module.Flat.flat_iff_torsion_eq_bot_of_isBezout

added theorem Module.Flat.flat_iff_torsion_eq_bot_of_valuationRing_localization_isMaximal

added theorem Module.Flat.isSMulRegular_of_isRegular

added theorem Module.Flat.isSMulRegular_of_nonZeroDivisors

added theorem Module.Flat.torsion_eq_bot

Modified Mathlib/RingTheory/Ideal/IsPrincipal.lean

added theorem Ideal.isoBaseOfIsPrincipal_apply

added theorem Ideal.subtype_isoBaseOfIsPrincipal_eq_mul