one_mem_commutatorSet

Mathlib.GroupTheory.Commutator.Basic

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

English

The identity element 1 of G lies in the commutatorSet G, since 1 = [1,1].

Русский

Единица группы G принадлежит commutatorSet(G), так как 1 = [1,1].

LaTeX

$$$ (1 : G) \\in commutatorSet(G) $$$

Lean4

theorem one_mem_commutatorSet : (1 : G) ∈ commutatorSet G :=
  ⟨1, 1, commutatorElement_self 1⟩

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

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

Разделы

Аффилиация

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