# Commit 2020-06-15 08:05 758806ec

View on Github →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.

Mathlib v3 is deprecated. Go to Mathlib v4

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.