Conjugacy of elements of finite groups #
instance
instFintypeConjClassesOfDecidableRelIsConj
{α : Type u_1}
[Monoid α]
[Fintype α]
[DecidableRel IsConj]
:
Fintype (ConjClasses α)
instance
conjugatesOf.fintype
{α : Type u_1}
[Monoid α]
[Fintype α]
[DecidableRel IsConj]
{a : α}
:
Fintype ↑(conjugatesOf a)
Equations
instance
ConjClasses.instFintypeElemCarrier
{α : Type u_1}
[Monoid α]
[Fintype α]
[DecidableRel IsConj]
{x : ConjClasses α}
: