Zulip Chat Archive
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):
Last updated: Dec 20 2023 at 11:08 UTC