mathlib

d91c8785 - chore(group_theory/group_action): introduce `smul_comm_class` (#4770)