commutator_def — Mathlib

English

The commutator of subgroups H1 and H2 is the same as the closure of the set of all commutators between elements of H1 and H2.

Русский

Определение коммутатора подгрупп: [H1, H2] = closure { g | ∃ h1∈H1, ∃ h2∈H2, [h1,h2] = g }.

LaTeX

$$$$ [H_1, H_2] = \\operatorname{cl}\\{ g \\mid \\exists h_1 \\in H_1, \\exists h_2 \\in H_2, [h_1, h_2] = g \\} $$$$

Lean4

theorem commutator_def (H₁ H₂ : Subgroup G) : ⁅H₁, H₂⁆ = closure {g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g} :=
  rfl

Похожие утверждения