[Merged by Bors] - feat(Projectivization/Colinear): Define colinearity for points in projective spaces#39786

Whysoserioushah wants to merge 14 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

Whysoserioushah:edison/projgeo4Whysoserioushah/mathlib4:edison/projgeo4Copy head branch name to clipboard