conjugation of group elements

[Alizter]

Here are the basics on conjugation in groups.

[Alizter]

I chose the convention y * x * y^ since that is how we conjugate elsewhere in the library already. I am however starting to think the other y^ * x * y might be better since it is more commonly used in group theory. Not sure.

[Alizter]

Perhaps the best way forward is to have both and use them whenever they are needed. Any result about one will become a result about the other in the opposite group.

[jdchristensen]

I chose the convention y * x * y^ since that is how we conjugate elsewhere in the library already. I am however starting to think the other y^ * x * y might be better since it is more commonly used in group theory. Not sure.

I think y * x * y^ is fine. It has the advantage that grp_conj is a homomorphism from the group to the group of self-equivalences rather than an anti-homomorphism.

Perhaps the best way forward is to have both and use them whenever they are needed. Any result about one will become a result about the other in the opposite group.

In the opposite group, it'll turn out to be y^ * (x * y), which is different from y^ * x * y. So there are really four choices here.

[Alizter]

I added this lemma when rebasing.

[jdchristensen]

This LGTM.