mathlib

90a44f6b - feat(linear_algebra/projective_space/subspace): defines subspaces of a projective space (#15391)

feat(linear_algebra/projective_space/subspace): defines subspaces of a projective space (#15391) This PR defines subspaces of a projective space, and shows that they form a complete lattice under inclusion. In an upcoming PR we show that there is an order-preserving bijection between the lattice of a subspaces of a projective space and the lattice of submodules of the underlying vector space.