Multiplicative version of NoZeroSMulDivisors?

Stream: maths

[Yury G. Kudryashov]

I noticed that docs#Subgroup.mem_closure_singleton_iff_existsUnique_zpow assumes a LinearOrderedCommGroup while actually it needs a ^ m = 1 → a = 1 ∨ m = 0. Should we add NoRoots, a multiplicative version of docs#NoZeroSMulDivisors ?

[Johan Commelin]

Or NoRootsOfUnity?

[Yury G. Kudryashov]

As @Yongle Hu pointed on Github, we already have this for Nat (the only relevant case, as we don't have typeclasses for a ^ (x + y) = a ^ x * a ^ y etc), and it's called docs#Monoid.IsTorsionFree

[Yury G. Kudryashov]

Unless someone comes with a better plan, I'm going to

• move the definition of Monoid.IsTorsionFree to a separate file (or to Group/Defs);
• reformulate the definition without without periodicPts;
• add instances from AddMonoid.IsTorsionFree M to NoZeroSMulDivisors Nat M and NoZeroSMulDivisors Int M;
• assume AddMoonoid.IsTorsionFree M instead of NoZeroSMulDivisors (Nat|Int) M
• reformulate docs#zpow_right_inj etc for Monoid.IsTorsionFree, as I did in #17133 with NoRootsOfUnity.

[Yury G. Kudryashov]

Since Monoid.IsTorsionFree is an existing typeclass, it will be easier to split this refactor into steps.

[Yury G. Kudryashov]

BTW, should we use Monoid.IsTorsionFree/AddMonoid.IsTorsionFree or IsMulTorsionFree/IsAddTorsionFree?

[Yaël Dillies]

I much prefer the latter