mathlib3

261a1953 - feat(group_theory/group_action/opposite): Add `smul_eq_mul_unop` (#12995)

feat(group_theory/group_action/opposite): Add `smul_eq_mul_unop` (#12995) This PR adds a simp-lemma `smul_eq_mul_unop`, similar to `op_smul_eq_mul` and `smul_eq_mul`. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>