English
For subgroups H1,H2 in G and K1,K2 in G', the commutator of H1.prod K1 and H2.prod K2 equals [H1,H2] . [K1,K2].
Русский
Для подгрупп H1,H2 в G и K1,K2 в G' имеет место: [H1.prod K1, H2.prod K2] = [H1,H2] . [K1,K2].
LaTeX
$$$$ [H_1 \\cdot K_1, H_2 \\cdot K_2] = [H_1,H_2] \\cdot [K_1,K_2]. $$$$
Lean4
theorem commutator_prod_prod (K₁ K₂ : Subgroup G') : ⁅H₁.prod K₁, H₂.prod K₂⁆ = ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆ :=
by
apply le_antisymm
· rw [commutator_le]
rintro ⟨p₁, p₂⟩ ⟨hp₁, hp₂⟩ ⟨q₁, q₂⟩ ⟨hq₁, hq₂⟩
exact ⟨commutator_mem_commutator hp₁ hq₁, commutator_mem_commutator hp₂ hq₂⟩
· rw [prod_le_iff]
constructor <;>
· rw [map_commutator]
apply commutator_mono <;>
simp [le_prod_iff, map_map, MonoidHom.fst_comp_inl, MonoidHom.snd_comp_inl, MonoidHom.fst_comp_inr,
MonoidHom.snd_comp_inr]
