Commutators of finite direct products

The commutator of a finite direct product is contained in the direct product of the commutators.

theorem Subgroup.commutator_pi_pi_of_finite {η : Type u_2} [Finite η] {Gs : η → Type u_3} [(i : η) → Group (Gs i)] (H K : (i : η) → Subgroup (Gs i)) : ⁅pi Set.univ H, pi Set.univ K⁆ = pi Set.univ fun (i : η) => ⁅H i, K i⁆

The commutator of a finite direct product is contained in the direct product of the commutators.

theorem AddSubgroup.addCommutator_pi_pi_of_finite {η : Type u_2} [Finite η] {Gs : η → Type u_3} [(i : η) → AddGroup (Gs i)] (H K : (i : η) → AddSubgroup (Gs i)) : ⁅pi Set.univ H, pi Set.univ K⁆ = pi Set.univ fun (i : η) => ⁅H i, K i⁆

The commutator of a finite direct product is contained in the direct product of the commutators.

instance Subgroup.instFGSubtypeMemCommutator {G : Type u_1} [Group G] [Finite ↑(commutatorSet G)] : Group.FG ↥(_root_.commutator G)

theorem Subgroup.rank_commutator_le_card (G : Type u_1) [Group G] [Finite ↑(commutatorSet G)] : Group.rank ↥(_root_.commutator G) ≤ Nat.card ↑(commutatorSet G)

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] : (center G).index ≤ Nat.card ↑(commutatorSet G) ^ Group.rank G

theorem card_commutatorSet_closureCommutatorRepresentatives {G : Type u_1} [Group G] : Nat.card ↑(commutatorSet ↥(closureCommutatorRepresentatives G)) = Nat.card ↑(commutatorSet G)

theorem card_commutator_closureCommutatorRepresentatives {G : Type u_1} [Group G] : Nat.card ↥(commutator ↥(closureCommutatorRepresentatives G)) = Nat.card ↥(commutator G)

instance instFiniteElemProdCommutatorRepresentatives {G : Type u_1} [Group G] [Finite ↑(commutatorSet G)] : Finite ↑(commutatorRepresentatives G)

instance closureCommutatorRepresentatives_fg {G : Type u_1} [Group G] [Finite ↑(commutatorSet G)] : Group.FG ↥(closureCommutatorRepresentatives G)

theorem rank_closureCommutatorRepresentatives_le (G : Type u_1) [Group G] [Finite ↑(commutatorSet G)] : Group.rank ↥(closureCommutatorRepresentatives G) ≤ 2 * Nat.card ↑(commutatorSet G)

instance instFiniteElemSubtypeMemSubgroupClosureCommutatorRepresentativesCommutatorSet {G : Type u_1} [Group G] [Finite ↑(commutatorSet G)] : Finite ↑(commutatorSet ↥(closureCommutatorRepresentatives G))