Conjugacy of elements of finite groups

@[instance_reducible]

instance instFintypeConjClassesOfDecidableRelIsConj {α : Type u_1} [Monoid α] [Fintype α] [DecidableRel IsConj] : Fintype (ConjClasses α)

Equations

• instFintypeConjClassesOfDecidableRelIsConj = Quotient.fintype (IsConj.setoid α)

instance instFiniteConjClasses {α : Type u_1} [Monoid α] [Finite α] : Finite (ConjClasses α)

@[instance_reducible]

instance instDecidableRelIsConjOfDecidableEqOfFintype {α : Type u_1} [Monoid α] [DecidableEq α] [Fintype α] : DecidableRel IsConj

Equations

• instDecidableRelIsConjOfDecidableEqOfFintype a b = { decide := decide (∃ a_1 ∈ Finset.univ, (fun (c : αˣ) => ↑c * a = b * ↑c) a_1), reflects_decide := ⋯ }

@[instance_reducible]

instance conjugatesOf.fintype {α : Type u_1} [Monoid α] [Fintype α] [DecidableRel IsConj] {a : α} : Fintype ↑(conjugatesOf a)

Equations

• conjugatesOf.fintype = Subtype.fintype (Membership.mem (conjugatesOf a))

@[instance_reducible]

instance ConjClasses.instFintypeElemCarrier {α : Type u_1} [Monoid α] [Fintype α] [DecidableRel IsConj] {x : ConjClasses α} : Fintype ↑x.carrier

Equations

• ConjClasses.instFintypeElemCarrier = Quotient.recOnSubsingleton x fun (x : α) => conjugatesOf.fintype