feat(linear_algebra/affine_space): more lemmas on directions of affine subspaces (#3377)
feat(linear_algebra/affine_space): more lemmas on directions of affine subspaces (#3377)

Add more lemmas on directions of affine subspaces, motivated by uses
for Euclidean geometry.






leanprover-community/mathlib,leanprover-community/mathlib