mathlib3

71320d9b - feat(group_theory/group_action/conj_act): smul_comm_class instances (#15876)

feat(group_theory/group_action/conj_act): smul_comm_class instances (#15876) Notably these instances give us access to conjugation as a linear map, enabling the pointwise scalar multiplication on submodules. I also moved the `forall` lemma to be next to the `rec` definition it is similar to.