commutatorElement

Mathlib.Algebra.Group.Commutator

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

← MathLib Explorer

English

The commutator of two elements g1 and g2 is defined as [g1,g2] = g1 g2 g1^{-1} g2^{-1}.

Русский

Коммутатор двух элементов g1 и g2 определяется как [g1,g2] = g1 g2 g1^{-1} g2^{-1}.

LaTeX

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

Lean4

/-- The commutator of two elements `g₁` and `g₂`. -/
instance commutatorElement {G : Type*} [Group G] : Bracket G G :=
  ⟨fun g₁ g₂ ↦ g₁ * g₂ * g₁⁻¹ * g₂⁻¹⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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