Commit 2022-03-28 20:38 261a1953

View on Github →

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.

Estimated changes

Modified src/group_theory/group_action/opposite.lean

added theorem mul_opposite.smul_eq_mul_unop

modified theorem op_smul_eq_mul