Commit 2026-09-30 14:37 e9626a55

refactor(Algebra/Group): fix the definition of torsion-free non-abelian groups (#42407) This PR redefines torsion-free to be that exponentiation by every non-zero element n : ℕ is injective on commuting elements (i.e., a * b = b * a → a ^ n = b ^ n → a = b). For commutative monoids, this is equivalent to a ^ n = b ^ n → a = b. For groups, this is equivalent to a ^ n = 1 → a = 1. Thus, this definition reconciles the notions of torsion-free for groups and commutative semigroups. This definition was taken from this mathoverflow answer: https://mathoverflow.net/a/377268/95685 Zulip thread: [#mathlib4 > Definition of `IsMulTorsionFree`](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Definition.20of.20.60IsMulTorsionFree.60/with/614317763) The old definition has been renamed to HasUniqueRoots and HasUniqueDiv (analogous to RootableBy and DivisibleBy).