mathlib

925ea07d - feat(linear_algebra/basic): add missing lemma finsupp.sum_smul_index_linear_map' (#6565)

feat(linear_algebra/basic): add missing lemma finsupp.sum_smul_index_linear_map' (#6565) See also [this Zulip conversation](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Sum.20is.20linear/near/229021943). cc @eric-wieser Co-authored-by: Adam Topaz <github@adamtopaz.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>