Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-04 16:21 fe21f5de

View on Github →

feat(group_theory/torsion): define torsion subgroups and show they're torsion (#12769) Also tidy up some linter errors and docstring for the module.

Estimated changes

Modified scripts/nolints.txt

Modified src/group_theory/torsion.lean

added theorem comm_monoid.torsion.is_torsion

added def comm_monoid.torsion

added theorem monoid.is_torsion.torsion_eq_top

added def monoid.is_torsion.torsion_mul_equiv

added def torsion.of_torsion

added def torsion

added theorem torsion_eq_torsion_submonoid