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.
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.