Documentation

Mathlib.Algebra.Group.Commutator

The bracket on a group given by commutator. #

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

The commutator of two elements g₁ and g₂.

Equations
  • commutatorElement = { bracket := fun 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₂⁻¹