mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

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

Open MichaelBlyth opened this issue 3 years ago • 2 comments

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

Open in Gitpod

MichaelBlyth avatar Aug 08 '22 15:08 MichaelBlyth

This PR/issue depends on:

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

mathlib-dependent-issues-bot avatar Aug 16 '22 19:08 mathlib-dependent-issues-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.

bors[bot] avatar Oct 11 '22 10:10 bors[bot]