Commit 2022-04-15 10:39 d13f291b

feat(group_theory/group_action/conj_act): conjugation by the units of a monoid (#13439) I suspect we can make this even more general in future by introducing a compatibility typeclass, but this is good enough for me for now. This also adds a stronger typeclass for the existing action of conj_act K where K is a division_ring.