The bracket on a group given by commutator.

Notation

After open scoped commutatorElement, ⁅g₁, g₂⁆ is syntax for g₁ * g₂ * g₁⁻¹ * g₂⁻¹.

@[reducible]

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

The commutator of two elements g₁ and g₂. This is a scoped instance in the commutatorElement namespace to avoid clashing with other brackets.

Equations

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

@[reducible]

def addCommutatorElement {G : Type u_1} [AddGroup G] : Bracket G G

The additive commutator of two elements g₁ and g₂. This is a scoped instance in the commutatorElement namespace to avoid clashing with other brackets

Equations

• addCommutatorElement = { 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₂⁻¹

theorem addCommutatorElement_def {G : Type u_1} [AddGroup G] (g₁ g₂ : G) : ⁅g₁, g₂⁆ = g₁ + g₂ + -g₁ + -g₂