Conjugacy of elements of finite groups #
instance
instFintypeConjClasses
{α : Type u_1}
[inst : Monoid α]
[inst : Fintype α]
[inst : DecidableRel IsConj]
:
Fintype (ConjClasses α)
Equations
- instFintypeConjClasses = Quotient.fintype (IsConj.setoid α)
instance
instFiniteConjClasses
{α : Type u_1}
[inst : Monoid α]
[inst : Finite α]
:
Finite (ConjClasses α)
instance
instDecidableRelIsConj
{α : Type u_1}
[inst : Monoid α]
[inst : DecidableEq α]
[inst : Fintype α]
:
DecidableRel IsConj
Equations
- instDecidableRelIsConj a b = inferInstanceAs (Decidable (∃ c, ↑c * a = b * ↑c))
instance
conjugatesOf.fintype
{α : Type u_1}
[inst : Monoid α]
[inst : Fintype α]
[inst : DecidableRel IsConj]
{a : α}
:
Fintype ↑(conjugatesOf a)
Equations
- conjugatesOf.fintype = Subtype.fintype fun x => x ∈ conjugatesOf a
instance
ConjClasses.instFintypeElemCarrier
{α : Type u_1}
[inst : Monoid α]
[inst : Fintype α]
[inst : DecidableRel IsConj]
{x : ConjClasses α}
:
Equations
- ConjClasses.instFintypeElemCarrier = Quotient.recOnSubsingleton x fun x => conjugatesOf.fintype