mathlib3 documentation

algebra.group.commutator

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₂⁻¹