Mathlib v3 is deprecated. Go to Mathlib v4

Theorem mul_opposite.smul_eq_mul_unop

Modification history

2022-03-28 20:38
src/group_theory/group_action/opposite.lean
feat(group_theory/group_action/opposite): Add `smul_eq_mul_unop` (#12995) …
Added mul_opposite.smul_eq_mul_unopView on Github →