Commit 2020-09-09 13:02 297a14e4
View on Github →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.