commutator_le_left

Mathlib.GroupTheory.Commutator.Basic

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

English

If H1 is normal, then [H1, H2] ≤ H1.

Русский

Если H1 нормальна, то [H1, H2] ≤ H1.

LaTeX

$$$$ [H_1, H_2] \\le H_1 $$$$

Lean4

theorem commutator_le_left [H₁.Normal] : ⁅H₁, H₂⁆ ≤ H₁ :=
  commutator_comm H₂ H₁ ▸ commutator_le_right H₂ H₁

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

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

Разделы

Аффилиация

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