mathlib3

3dcc1689 - feat(linear_algebra/projective_space/basic): The projectivization of a vector space. (#12438)

feat(linear_algebra/projective_space/basic): The projectivization of a vector space. (#12438) This provides the initial definitions for the projective space associated to a vector space. Future work: - Linear subspaces of projective spaces, connection with subspaces of the vector space, etc. - The incidence geometry structure of a projective space. - The fundamental theorem of projective geometry. I will tag this PR as RFC for now. If you see something missing from this *initial* PR, please let me know!