The bracket on a group given by commutator. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[protected, instance]

def commutator_element {G : Type u_1} [group G] :

The commutator of two elements g₁ and g₂.

Equations

theorem commutator_element_def {G : Type u_1} [group G] (g₁ g₂ : G) :

⁅g₁, g₂⁆ = g₁ * g₂ * g₁⁻¹ * g₂⁻¹