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.