Commit 2024-02-29 21:30 a424c094

View on Github →

feat: IsTorsionFree M ↔ NoZeroSMulDivisors ℕ M (#10918) and some subgroup results. From PFR

Estimated changes

Modified Mathlib/Algebra/Module/Basic.lean

Modified Mathlib/Algebra/Module/Torsion.lean

deleted theorem Submodule.AddMonoid.IsTorsionFree_iff_noZeroSMulDivisors

Modified Mathlib/GroupTheory/Subgroup/Pointwise.lean

added theorem coe_div_coe

added theorem coe_mul_coe

Modified Mathlib/GroupTheory/Torsion.lean

added theorem IsTorsionFree.of_noZeroSMulDivisors

added theorem isTorsionFree_iff_noZeroSMulDivisors_int

added theorem isTorsionFree_iff_noZeroSMulDivisors_nat