commutatorElement_def

Mathlib.Algebra.Group.Commutator

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

English

The commutator bracket [g1,g2] is equal to g1 g2 g1^{-1} g2^{-1}.

Русский

Скобка коммутатора [g1,g2] равна g1 g2 g1^{-1} g2^{-1}.

LaTeX

$$$ [g_1,g_2] = g_1 g_2 g_1^{-1} g_2^{-1} $$$

Lean4

theorem commutatorElement_def {G : Type*} [Group G] (g₁ g₂ : G) : ⁅g₁, g₂⁆ = g₁ * g₂ * g₁⁻¹ * g₂⁻¹ :=
  rfl

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

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

Разделы

Аффилиация

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