Theorem CommGroup.mem_primaryComponent

Modification history

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