Documentation

Mathlib.Algebra.Group.ConjFinite

Conjugacy of elements of finite groups #

instance instFintypeConjClasses {α : Type u_1} [inst : Monoid α] [inst : Fintype α] [inst : DecidableRel IsConj] :
Equations
instance instDecidableRelIsConj {α : Type u_1} [inst : Monoid α] [inst : DecidableEq α] [inst : Fintype α] :
Equations
instance conjugatesOf.fintype {α : Type u_1} [inst : Monoid α] [inst : Fintype α] [inst : DecidableRel IsConj] {a : α} :
Equations
instance ConjClasses.instFintypeElemCarrier {α : Type u_1} [inst : Monoid α] [inst : Fintype α] [inst : DecidableRel IsConj] {x : ConjClasses α} :
Equations