Theorem smul_smul
Modification history
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_smulView on Github →2020-11-11 22:13
src/group_theory/group_action.lean
refactor(group_theory/group_action): Break the file into three pieces (#4936) …
Modified smul_smulView on Github →2020-01-26 13:49
src/algebra/module.lean
refactor(*): refactor `sum_smul`/`smul_sum` (#1910) …
Modified smul_smulView on Github →2018-11-05 10:47
algebra/module.lean
feat(linear_algebra,ring_theory): refactoring modules (#456) …
Modified smul_smulView on Github →2017-11-10 11:32
algebra/module.lean
chore(algebra/module): hide ring parameters, vector_space is no a proper class, remove dual, change variables to implicits …
Modified smul_smulView on Github →