feat(linear_algebra/affine_space): more lemmas (#4055)
Add some more lemmas about affine spaces. One,
`affine_span_insert_affine_span`, is extracted from the proof of
`exists_unique_dist_eq_of_affine_independent` as it turned out to be
useful elsewhere.
