Theorem finset.smul_sum
Modification history
2022-04-19 14:04
src/group_theory/group_action/basic.lean
refactor(group_theory/group_action/big_operators): extract to a new file (#13340) …
Modified finset.smul_sumView 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 finset.smul_sumView on Github →2020-01-26 13:49
src/group_theory/group_action.lean
refactor(*): refactor `sum_smul`/`smul_sum` (#1910) …
Modified finset.smul_sumView on Github →2019-10-10 11:14
src/linear_algebra/basic.lean
chore(linear_algebra): rename type variables (#1521) …
Modified finset.smul_sumView on Github →