commutator_bot_left

Mathlib.GroupTheory.Commutator.Basic

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

English

The commutator of the bottom subgroup with H1 is the bottom subgroup: [⊥, H1] = ⊥.

Русский

Коммутатор нулевой подгруппы с H1 равен нулю: [⊥, H1] = ⊥.

LaTeX

$$$$ [\\perp, H_1] = \\perp $$$$

Lean4

@[simp]
theorem commutator_bot_left : ⁅(⊥ : Subgroup G), H₁⁆ = ⊥ :=
  le_bot_iff.mp (commutator_le_left ⊥ H₁)

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

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

Разделы

Аффилиация

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