The commutator of a finite direct product is contained in the direct product of the commutators.
instance
Subgroup.finiteIndex_center
{G : Type u_1}
[Group G]
[Finite ↑(commutatorSet G)]
[Group.FG G]
:
(center G).FiniteIndex
theorem
Subgroup.index_center_le_pow
(G : Type u_1)
[Group G]
[Finite ↑(commutatorSet G)]
[Group.FG G]
:
instance
instFiniteElemProdCommutatorRepresentatives
{G : Type u_1}
[Group G]
[Finite ↑(commutatorSet G)]
:
theorem
rank_closureCommutatorRepresentatives_le
(G : Type u_1)
[Group G]
[Finite ↑(commutatorSet G)]
:
instance
instFiniteElemSubtypeMemSubgroupClosureCommutatorRepresentativesCommutatorSet
{G : Type u_1}
[Group G]
[Finite ↑(commutatorSet G)]
: