Commit 2025-12-17 04:27 a1fc8a73

View on Github →

chore(GroupTheory/Torsion): delete deprecated declarations (#32843) These are on my way for #30563.

Estimated changes

Modified Mathlib/GroupTheory/Torsion.lean

deleted theorem AddMonoid.IsTorsionFree.of_noZeroSMulDivisors

deleted theorem AddMonoid.isTorsionFree_iff_noZeroSMulDivisors_int

deleted theorem AddMonoid.isTorsionFree_iff_noZeroSMulDivisors_nat

deleted theorem Monoid.IsTorsion.not_torsion_free

deleted theorem Monoid.IsTorsionFree.not_torsion

deleted theorem Monoid.IsTorsionFree.prod

deleted theorem Monoid.IsTorsionFree.quotient_torsion

deleted theorem Monoid.IsTorsionFree.subgroup

deleted def Monoid.IsTorsionFree

deleted theorem Monoid.isTorsionFree_iff_torsion_eq_bot

deleted theorem Monoid.isTorsionFree_of_subsingleton

deleted theorem Monoid.not_isTorsionFree_iff