Theorem smul_eq_mul
Modification history
2021-06-13 06:04
src/group_theory/group_action/defs.lean
feat(group_theory/group_action/defs): add `has_mul.to_has_scalar` and relax typeclass in `smul_mul_smul` (#7885)
Modified smul_eq_mulView on Github →2021-04-02 21:56
src/group_theory/group_action/defs.lean
refactor(algebra/add_torsor): use `to_additive` for `add_action` (#6914)
Modified smul_eq_mulView on Github →2021-03-01 10:35
src/algebra/module/basic.lean
fix(group_action/defs): make mul_action.regular an instance (#6241) …
Modified smul_eq_mulView on Github →2020-04-13 05:19
src/algebra/module.lean
chore(algebra/module): rename type vars, minor cleanup, add module docstring (#2392) …
Modified smul_eq_mulView on Github →