commutator — Mathlib

English

The commutator of two subgroups H1 and H2 is the closure of all commutators [h1, h2] with h1 ∈ H1 and h2 ∈ H2.

Русский

Коммутатор двух подгрупп H1 и H2 — порожденная замкнутая подгруппа множество всех [h1, h2] с h1 ∈ H1, h2 ∈ H2.

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

/-- The commutator of two subgroups `H₁` and `H₂`. -/
instance commutator : Bracket (Subgroup G) (Subgroup G) :=
  ⟨fun H₁ H₂ => closure {g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g}⟩

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