commutatorElement_inv

Mathlib.GroupTheory.Commutator.Basic

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

English

The inverse of a commutator reverses the order: [g1, g2]^{-1} = [g2, g1].

Русский

Обратный коммутатор меняет порядок: [g1, g2]^{-1} = [g2, g1].

LaTeX

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

Lean4

@[simp]
theorem commutatorElement_inv : ⁅g₁, g₂⁆⁻¹ = ⁅g₂, g₁⁆ := by
  simp_rw [commutatorElement_def, mul_inv_rev, inv_inv, mul_assoc]

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

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

Разделы

Аффилиация

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