Commit 2020-06-15 08:05 758806ecView 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.
added theorem affine_subspace.direction_mk_of_point_of_direction
added theorem affine_subspace.ext
added theorem affine_subspace.ext_of_direction_eq
added theorem affine_subspace.mem_mk_of_point_of_direction
added def affine_subspace.mk_of_point_of_direction
added theorem affine_subspace.mk_of_point_of_direction_eq