mathlib3

fc5e8cb0 - chore(algebra/group): missed generalizations to mul_one_class (#7259)

chore(algebra/group): missed generalizations to mul_one_class (#7259) This adds a missing `ulift` instance, relaxes some lemmas about `semiconj` and `commute` to apply more generally, and broadens the scope of the definitions `monoid_hom.apply` and `ulift.mul_equiv`.