mathlib3
fe21f5de - feat(group_theory/torsion): define torsion subgroups and show they're torsion (#12769)

Commit

3 years ago

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

Author

Julian

Parents