Commit 2025-07-27 09:45 bacb344a

View on Github →

chore: replace Monoid.IsTorsionFree with IsMulTorsionFree (#24311) From Toric

Estimated changes

Modified Mathlib/Algebra/Group/Torsion.lean

Modified Mathlib/Algebra/NoZeroSMulDivisors/Defs.lean

Modified Mathlib/Combinatorics/Additive/CauchyDavenport.lean

deleted theorem cauchy_davenport_mul_of_isTorsionFree

added theorem cauchy_davenport_of_isMulTorsionFree

Modified Mathlib/GroupTheory/Order/Min.lean

modified theorem Monoid.minOrder_eq_top

added theorem Monoid.minOrder_eq_top_iff

modified theorem Monoid.minOrder_le_natCard

Modified Mathlib/GroupTheory/Torsion.lean

Modified Mathlib/Topology/Instances/ZMultiples.lean