mathlib

c4afaddc - feat(linear_algebra/projective_space): add some basic API and instance