commutatorElement_one_left

Mathlib.GroupTheory.Commutator.Basic

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

English

Let G be a group and g ∈ G. The commutator of the identity with g is the identity: [e, g] = e.

Русский

Пусть G — группа и g ∈ G. Коммутатор единицы и g равен единице: [e, g] = e.

LaTeX

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

Lean4

@[simp]
theorem commutatorElement_one_left : ⁅(1 : G), g⁆ = 1 :=
  (Commute.one_left g).commutator_eq

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

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

Разделы

Аффилиация

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