mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(Algebra): additive `n`-torsion subgroups

Open wupr opened this issue 10 months ago • 1 comments

For an AddCommGroup A and a natural number n,

  • Define AddSubgroup.torsionBy A n using Submodule.torsionBy.
  • Define a scoped notation A[n]
  • Equip AddSubgroup.torsionBy A n with a ZMod n-module structure.

Open in Gitpod

wupr avatar Mar 28 '24 12:03 wupr