Additivizing IsTorsion

Stream: mathlib4

[Ruben Van de Velde]

docs#Monoid.IsTorsion is translated to docs#AddMonoid.IsTorsion, so naturally we refer to it in the following lemmas:

• AddIsTorsion.quotient_iff, AddIsTorsion.of_surjective, AddIsTorsion.extension_closed
• ExponentExists.is_add_torsion, is_add_torsion_of_finite
• IsAddTorsion.exponentExists
• IsTorsion.addGroup
• AddMonoid.not_isTorsion_iff

Who wants to suggest a naming convention?

cc @Yaël Dillies

[Yaël Dillies]

What about renaming

• Monoid.IsTorsion → IsMulTorsion
• AddMonoid.IsTorsion → IsAddTorsion

[Yaël Dillies]

In general, definitions in the Monoid/AddMonoid namespace are very annoying to refer to. This is a problem.

[Ruben Van de Velde]

(Incidentally, _root_.ExponentExists.isTorsion doesn't work in dot notation because it's about Monoid.ExponentExists)