commutator_le_right — Mathlib

English

The commutator of subgroups H1 and H2 is defined as the closure of the set of all commutators [h1,h2] with h1∈H1, 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

theorem commutator_le_right [h : H₂.Normal] : ⁅H₁, H₂⁆ ≤ H₂ :=
  commutator_le.mpr fun g₁ _h₁ g₂ h₂ => H₂.mul_mem (h.conj_mem g₂ h₂ g₁) (H₂.inv_mem h₂)

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