Commit 2021-07-12 12:59 695cb07b

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.