Documentation

Mathlib.Algebra.Group.ConjFinite

Conjugacy of elements of finite groups #

source
instance instFintypeConjClassesOfDecidableRelIsConj {α : Type u_1} [Monoid α] [Fintype α] [DecidableRel IsConj] :
Fintype (ConjClasses α)
Equations
    source
    instance instFiniteConjClasses {α : Type u_1} [Monoid α] [Finite α] :
    Finite (ConjClasses α)
    source
    instance instDecidableRelIsConjOfDecidableEqOfFintype {α : Type u_1} [Monoid α] [DecidableEq α] [Fintype α] :
    DecidableRel IsConj
    Equations
      source
      instance conjugatesOf.fintype {α : Type u_1} [Monoid α] [Fintype α] [DecidableRel IsConj] {a : α} :
      Fintype ↑(conjugatesOf a)
      Equations
        source
        instance ConjClasses.instFintypeElemCarrier {α : Type u_1} [Monoid α] [Fintype α] [DecidableRel IsConj] {x : ConjClasses α} :
        Fintype ↑x.carrier
        Equations