commutator_mem_commutator

Mathlib.GroupTheory.Commutator.Basic

URI: https://scilib.ai/kg/mathlib#Subgroup.commutator_mem_commutator

English

If h1 ∈ H1 and h2 ∈ H2, then the commutator [h1, h2] lies in [H1, H2].

Русский

Если h1 ∈ H1 и h2 ∈ H2, то [h1, h2] принадлежит [H1, H2].

LaTeX

$$$$ \\text{If } h_1 \\in H_1 \\text{ and } h_2 \\in H_2, \\, [h_1,h_2] \\in [H_1,H_2]. $$$$

Lean4

theorem commutator_mem_commutator (h₁ : g₁ ∈ H₁) (h₂ : g₂ ∈ H₂) : ⁅g₁, g₂⁆ ∈ ⁅H₁, H₂⁆ :=
  subset_closure ⟨g₁, h₁, g₂, h₂, rfl⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru