Documentation

Mathlib.GroupTheory.Commutator.Finite

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_1} [Finite η] {Gs : ηType u_2} [(i : η) → Group (Gs i)] (H : (i : η) → Subgroup (Gs i)) (K : (i : η) → Subgroup (Gs i)) :
Subgroup.pi Set.univ H, Subgroup.pi Set.univ K = Subgroup.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.