mathlib3 documentation

algebra.group.conj_finite

Conjugacy of elements of finite groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
@[protected, instance]
def conj_classes.fintype {α : Type u_1} [monoid α] [fintype α] [decidable_rel is_conj] :
fintype (conj_classes α)
Equations
source
@[protected, instance]
def conj_classes.finite {α : Type u_1} [monoid α] [finite α] :
finite (conj_classes α)
source
@[protected, instance]
def is_conj.decidable_rel {α : Type u_1} [monoid α] [decidable_eq α] [fintype α] :
decidable_rel is_conj
Equations
source
@[protected, instance]
def conjugates_of.fintype {α : Type u_1} [monoid α] [fintype α] [decidable_rel is_conj] {a : α} :
fintype ↥(conjugates_of a)
Equations
source
@[protected, instance]
def conj_classes.carrier.fintype {α : Type u_1} [monoid α] [fintype α] [decidable_rel is_conj] {x : conj_classes α} :
fintype ↥(x.carrier)
Equations