mathlib

1e82f5ec - feat(linear_algebra/projectivization/independence): defines (in)dependence of points in projective space (#14542)

feat(linear_algebra/projectivization/independence): defines (in)dependence of points in projective space (#14542) This PR only provides definitions and basic lemmas. In an upcoming pull request we use this to prove the axioms for an abstract projective space. Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com> Co-authored-by: Oliver Nash <github@olivernash.org> Co-authored-by: Adam Topaz <github@adamtopaz.com>