Abelian subgroup dividing order

Stream: Is there code for X?

[Bolton Bailey]

For an abelian group and natural n, we can take a subgroup of all the elements with order dividing n. Does this subgroup have a name in math, and is it in mathlib?

[Kevin Buzzard]

That's the n-torsion $A[n]$.

[Johan Commelin]

I don't think it's in mathlib yet.

[Johan Commelin]

Although you can define it as the kernel of multiplication by $n$. So that would be something like (smul_hom n).ker, modulo naming issues.

[Kevin Buzzard]

I think @Pierre-Alexandre Bazin has been using it in his ongoing work on the structure theorem for fg modules over a PID