## Stream: maths

### Topic: Conjugacy Classes

#### Aaron Anderson (Mar 26 2021 at 03:48):

For multiple purposes in representation theory, I find myself wanting to work with is_conj.

#### Aaron Anderson (Mar 26 2021 at 03:49):

Currently, is_conj is only defined on groups, but I'd like to be able to talk about, say, two matrices being conjugate. Does anyone see any problems with refactoring the definition of is_conj as I've done at branch#monoid_conj to involve units?

#### Aaron Anderson (Mar 26 2021 at 03:51):

Secondly, I'd really like to use the quotient type of conjugacy classes. Does is_conj exist anywhere as a setoid that I've just missed? If not, should I add it right at algebra.group.conj?

#### Johan Commelin (Mar 26 2021 at 05:17):

@Christopher Hughes I think you've worked most with is_conj.

#### Aaron Anderson (Mar 26 2021 at 17:21):

#6896

Last updated: May 09 2021 at 10:11 UTC