Theorem CommMonoid.mem_primaryComponent

Modification history

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