mathlib3

9fcf391e - chore(group_theory/group_action/basic): relax monoid to mul_one_class (#15051)