mathlib3

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