mathlib3

feat(linear_algebra/projective_space): add some basic API and instances

#14059

Open