English
Conjugating a commutator by a third element produces a commutator of the conjugates: [g3 g1 g3^{-1}, g3 g2 g3^{-1}].
Русский
Сопряжение коммутатора элементом g3 даёт коммутатор сопряжённых элементов: ...
LaTeX
$$$$ g_3 g_1 g_3^{-1},\\; g_3 g_2 g_3^{-1} $$$$
Lean4
instance commutator_normal [h₁ : H₁.Normal] [h₂ : H₂.Normal] : Normal ⁅H₁, H₂⁆ :=
by
let base : Set G := {x | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = x}
change (closure base).Normal
suffices h_base : base = Group.conjugatesOfSet base by
rw [h_base]
exact Subgroup.normalClosure_normal
refine Set.Subset.antisymm Group.subset_conjugatesOfSet fun a h => ?_
simp_rw [Group.mem_conjugatesOfSet_iff, isConj_iff] at h
rcases h with ⟨b, ⟨c, hc, e, he, rfl⟩, d, rfl⟩
exact ⟨_, h₁.conj_mem c hc d, _, h₂.conj_mem e he d, (conjugate_commutatorElement c e d).symm⟩
