Mathlib.Algebra.Group.Commutator

Module docstring

{"# The bracket on a group given by commutator. "}

commutatorElement instance

{G : Type*} [Group G] : Bracket G G

Full source

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

Commutator Bracket in a Group

Informal description

For any group $G$, the commutator bracket operation $\lbrack g_1, g_2 \rbrack = g_1 g_2 g_1^{-1} g_2^{-1}$ is defined for any two elements $g_1, g_2 \in G$.

commutatorElement_def theorem

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

Full source

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

Commutator Bracket Definition: $\lbrack g_1, g_2 \rbrack = g_1 g_2 g_1^{-1} g_2^{-1}$

Informal description

For any group $G$ and any two elements $g_1, g_2 \in G$, the commutator bracket $\lbrack g_1, g_2 \rbrack$ is equal to $g_1 g_2 g_1^{-1} g_2^{-1}$.