commutator_bot_right

Mathlib.GroupTheory.Commutator.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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