Theorem CommGroup.mem_torsion

Modification history

2023-08-02 23:55
Mathlib/GroupTheory/Torsion.lean
feat(NumberTheory.NumberField.Units): add torsion subgroup (#5748) …
Added CommGroup.mem_torsionView on Github →