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.

@[protected, instance]
def conj_classes.finite {α : Type u_1} [monoid α] [finite α] :
@[protected, instance]
Equations
@[protected, instance]
Equations