HepLean Documentation
Mathlib
.
Algebra
.
Group
.
Commutator
Search
Google site search
return to top
source
Imports
Init
Mathlib.Data.Bracket
Mathlib.Algebra.Group.Defs
Imported by
commutatorElement
commutatorElement_def
The bracket on a group given by commutator.
#
source
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₂
⁻¹
}
source
theorem
commutatorElement_def
{G :
Type
u_1}
[
Group
G
]
(g₁ g₂ :
G
)
:
⁅
g₁
,
g₂
⁆
=
g₁
*
g₂
*
g₁
⁻¹
*
g₂
⁻¹