Documentation

Mathlib.Algebra.Group.ConjFinite

Conjugacy of elements of finite groups #

instance instFintypeConjClasses {α : Type u_1} [Monoid α] [Fintype α] [DecidableRel IsConj] :
Equations
instance instFiniteConjClasses {α : Type u_1} [Monoid α] [Finite α] :
Equations
instance instDecidableRelIsConj {α : Type u_1} [Monoid α] [DecidableEq α] [Fintype α] :
Equations
instance conjugatesOf.fintype {α : Type u_1} [Monoid α] [Fintype α] [DecidableRel IsConj] {a : α} :
Equations
Equations