feat(linear_algebra/affine_space/combination): `sdiff`, `subtype`, `filter` lemmas (#16644)
feat(linear_algebra/affine_space/combination): `sdiff`, `subtype`, `filter` lemmas (#16644)

Add various lemmas about affine combinations in relation to subsets of the index type extracted with `sdiff`, `subtype` or `filter` (largely analogous to such lemmas present for `finset.sum`).







leanprover-community/mathlib,leanprover-community/mathlib