feat(linear_algebra/affine_space): more lemmas (#4127)
Add another batch of lemmas relating to affine spaces. These include
factoring out `vector_span_mono` as a combination of two other lemmas
that's used several times, and additional variants of lemmas relating
to finite-dimensional subspaces.
