[Merged by Bors] - feat(LinearAlgebra/Projectivization/Subspace): correspondence between linear and projective subspaces#26909

gasparattila wants to merge 4 commits intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

gasparattila:proj-subspace-isogasparattila/mathlib4:proj-subspace-isoCopy head branch name to clipboard