Commit 2026-07-24 18:27 26245e68

View on Github →

chore(GroupTheory/Torsion): rename IsTorsion to IsMulTorsion (#41213) GroupTheory/Torsion.lean has some bad to_additive translations. This PR fixes this by renaming Monoid.IsTorsion to IsMulTorsion and AddMonoid.IsTorsion to IsAddTorsion. This also aligns better with IsMulTorsionFree and IsAddTorsionFree. This PR has a lot of deprecations, but you can check the lean-aware declarations diff to make sure I didn't miss anything.

Estimated changes

modified theorem CommGroup.freeRank_eq_zero
deleted theorem ExponentExists.isTorsion
added theorem IsMulTorsion.subgroup
added def IsMulTorsion
deleted theorem IsTorsion.exponentExists
deleted theorem IsTorsion.of_surjective
deleted theorem IsTorsion.quotient_iff
deleted theorem IsTorsion.subgroup
deleted def Monoid.IsTorsion
deleted theorem Monoid.not_isTorsion_iff
deleted def Torsion.ofTorsion
added theorem isMulTorsion_of_finite
deleted theorem isTorsion_of_finite
added theorem not_isMulTorsion_iff