mathlib

d13f291b - feat(group_theory/group_action/conj_act): conjugation by the units of a monoid (#13439)

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`.