Theorem CommGroup.mem_primaryComponent_iff_orderOf

Modification history

2026-05-23 13:48
Mathlib/GroupTheory/Torsion.lean
refactor(GroupTheory/Torsion): make primaryComponent total (#39484) …
Added CommGroup.mem_primaryComponent_iff_orderOfView on Github →