Conjugacy of elements of finite groups

ink

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

Equations

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

ink

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

Equations

• @instFiniteConjClasses = @instFiniteConjClasses.proof_1

ink

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

Equations

• instDecidableRelIsConj a b = inferInstanceAs (Decidable (∃ c, ↑c * a = b * ↑c))

ink

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

ink

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

Equations

• ConjClasses.instFintypeElemCarrier = Quotient.recOnSubsingleton x fun x => conjugatesOf.fintype