Commit 2024-10-08 17:07 3a3a3ef5

View on Github →

feat: IsTorsionFree ↔ NoZeroSMulDivisors aliases (#17307) Also fix a few lemma names that were accidentally unnamespaced. From PFR

Estimated changes

Modified Mathlib/GroupTheory/Torsion.lean

added theorem AddMonoid.IsTorsionFree.of_noZeroSMulDivisors

added theorem AddMonoid.isTorsionFree_iff_noZeroSMulDivisors_int

added theorem AddMonoid.isTorsionFree_iff_noZeroSMulDivisors_nat

deleted theorem IsTorsion.not_torsion_free

deleted theorem IsTorsionFree.not_torsion

deleted theorem IsTorsionFree.of_noZeroSMulDivisors

deleted theorem IsTorsionFree.prod

deleted theorem IsTorsionFree.quotient_torsion

deleted theorem IsTorsionFree.subgroup

added theorem Monoid.IsTorsion.not_torsion_free

added theorem Monoid.IsTorsionFree.not_torsion

added theorem Monoid.IsTorsionFree.prod

added theorem Monoid.IsTorsionFree.quotient_torsion

added theorem Monoid.IsTorsionFree.subgroup

deleted theorem isTorsionFree_iff_noZeroSMulDivisors_int

deleted theorem isTorsionFree_iff_noZeroSMulDivisors_nat