The bracket on a group given by commutator.

instance commutatorElement {G : Type u_1} [Group G] : Bracket G G

The commutator of two elements g₁ and g₂.

Equations

• commutatorElement = { bracket := fun (g₁ g₂ : G) => g₁ * g₂ * g₁⁻¹ * g₂⁻¹ }

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