Commit 2021-03-11 06:05 925ea07d
View on Github →feat(linear_algebra/basic): add missing lemma finsupp.sum_smul_index_linear_map' (#6565) See also this Zulip conversation. cc @eric-wieser
feat(linear_algebra/basic): add missing lemma finsupp.sum_smul_index_linear_map' (#6565) See also this Zulip conversation. cc @eric-wieser