Commit 2024-08-22 13:52 06e67b6e

feat(Algebra): additive n-torsion subgroups (#11742) For an AddCommGroup A and an integer n,

• Define AddSubgroup.torsionBy A n using Submodule.torsionBy;
• Define a scoped notation A[n]. Additionally, for a natural number n,
• Equip A[n] with a ZMod n-module structure.