Conjugacy of group elements #
See also MulAut.conj
and Quandle.conj
.
theorem
conj_injective
{α : Type u}
[Group α]
{x : α}
:
Function.Injective fun (g : α) => x * g * x⁻¹
The quotient type of conjugacy classes of a group.
Equations
Instances For
Equations
theorem
ConjClasses.exists_rep
{α : Type u}
[Monoid α]
(a : ConjClasses α)
:
∃ (a0 : α), ConjClasses.mk a0 = a
def
ConjClasses.map
{α : Type u}
{β : Type v}
[Monoid α]
[Monoid β]
(f : α →* β)
:
ConjClasses α → ConjClasses β
A MonoidHom
maps conjugacy classes of one group to conjugacy classes of another.
Equations
Instances For
theorem
ConjClasses.map_surjective
{α : Type u}
{β : Type v}
[Monoid α]
[Monoid β]
{f : α →* β}
(hf : Function.Surjective ⇑f)
:
@[instance 900]
instance
ConjClasses.instDecidableEqOfDecidableRelIsConj
{α : Type u}
[Monoid α]
[DecidableRel IsConj]
: