mathlib3

fa46ef10 - feat(linear_algebra/affine_space/combination): vsub distributivity lemmas (#10786)

feat(linear_algebra/affine_space/combination): vsub distributivity lemmas (#10786) Add lemmas about weighted sums of `-ᵥ` expressions in terms of `weighted_vsub_of_point`, `weighted_vsub` and `affine_combination`, with special cases where the points on one side of the subtractions are constant, and lemmas about those three functions for constant points used to prove those special cases. These were suggested by one of the lemmas in #10632; the lemma `affine_basis.vsub_eq_coord_smul_sum` is a very specific case, but showed up that these distributivity lemmas were missing (and should follow immediately from `sum_smul_const_vsub_eq_vsub_affine_combination` in this PR).