Mathlib v3 is deprecated. Go to Mathlib v4

Theorem op_smul_eq_mul

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) …
Modified op_smul_eq_mulView on Github →
2022-01-04 13:36
src/group_theory/group_action/opposite.lean
feat(algebra/opposites): add `add_opposite` (#11080) …
Modified op_smul_eq_mulView on Github →
2021-11-22 11:23
src/group_theory/group_action/opposite.lean
chore(algebra/opposites): split group actions and division_ring into their own files (#10383) …
Added op_smul_eq_mulView on Github →