conjugate_commutatorElement — Mathlib

English

Conjugating the commutator by g3 yields the commutator of the conjugated elements: g3 [g1, g2] g3^{-1} = [g3 g1 g3^{-1}, g3 g2 g3^{-1}].

Русский

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

LaTeX

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

Lean4

theorem conjugate_commutatorElement : g₃ * ⁅g₁, g₂⁆ * g₃⁻¹ = ⁅g₃ * g₁ * g₃⁻¹, g₃ * g₂ * g₃⁻¹⁆ :=
  map_commutatorElement (MulAut.conj g₃).toMonoidHom g₁ g₂

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