mathlib3

b8e7a8d9 - 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`).