Commit 2025-04-22 11:54 7cf4690a

feat: torsion-free monoids (#22962) Behind this click-baity title, there is the fact that Monoid.IsTorsionFree is incorrect for torsion-free monoids. Indeed, if n ≠ 0 then ∀ a : α, n • a = 0 → a = 0 is equivalent to ∀ a b : α, n • a = n • b → a = b only if α is a group. If α is a monoid (possibly even cancellative!), then the ∀ a : α, n • a = 0 → a = 0 condition is quite weak. This PR introduces this new definition under the names IsAddTorsionFree/IsMulTorsionFree. Several things to note:

• It is a class, while Monoid.IsTorsionFree is not.
• It is outside of the Monoid/AddMonoid namespace. My thought is that people who care about torsion-free groups will prefer writing IsAddTorsionFree G over Monoid.IsTorsionFree.
• I am making a new file. This is because the existing definitions talk about order of an element, which is a much more advanced notion than the new one I am offering.
• I am not changing the existing definition in this PR. This will be done in a later PR. The new imports just come from making #min_imports and mk_iff available earlier. From Toric