mathlib3

48765fae - feat(linear_algebra/affine_space/combination): explicit weights for points, subtractions and `line_map` (#17660)

feat(linear_algebra/affine_space/combination): explicit weights for points, subtractions and `line_map` (#17660) Add a series of definitions and associated API for explicitly representing a single point, the subtraction of two points or the result of `line_map` as an affine combination (over a `finset` containing the relevant points). Also add `weighted_vsub_of_point_const_smul` and `weighted_vsub_const_smul` for use in proving one of the API lemmas.