mathlib

695cb07b - feat({data,linear_algebra}/{finsupp,dfinsupp}): add `{add_submonoid,submodule}.[d]finsupp_sum_mem` (#8269)

feat({data,linear_algebra}/{finsupp,dfinsupp}): add `{add_submonoid,submodule}.[d]finsupp_sum_mem` (#8269) These lemmas are trivial consequences of the finset lemmas, but having them avoids having to unfold `[d]finsupp.sum`. `dfinsupp_sum_add_hom_mem` is particularly useful because this one has some messy decidability arguments to eliminate.