mathlib3

feat(algebra/group/conj): conjugacy class as finset

#9843

Open