feat(linear_algebra/projective_space/subspace): adds constructors for projective subspaces

[MichaelBlyth]

This PR adds new ways to construct projective subspaces. This PR also adds lemmas which show that for a projective subspace, any nonzero linear combination of vectors, where each vector represents a point in the subspace, also represents a point in the subspace.

---

• [x] depends on: #15596

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#15596~~ By Dependent Issues (🤖). Happy coding!

[bors[bot]]

:v: MichaelBlyth can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.