commutatorElement_self

Mathlib.GroupTheory.Commutator.Basic

URI: https://scilib.ai/kg/mathlib#commutatorElement_self

English

In any group, the commutator of an element with itself is the identity: [g, g] = e.

Русский

В любой группе коммутатор элемента с самим собой равен единице: [g, g] = e.

LaTeX

$$$$ [g, g] = e $$$$

Lean4

@[simp]
theorem commutatorElement_self : ⁅g, g⁆ = 1 :=
  (Commute.refl g).commutator_eq

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

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

Разделы

Аффилиация

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