mathlib

758806ec - feat(linear_algebra/affine_space): more on affine subspaces (#3076)

feat(linear_algebra/affine_space): more on affine subspaces (#3076) Add extensionality lemmas for affine subspaces, and a constructor to make an affine subspace from a point and a direction.