[Merged by Bors] - feat(Projectivization/Independence): add lemma about independence#39778

Whysoserioushah wants to merge 3 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

Whysoserioushah:edison/projgeo3Whysoserioushah/mathlib4:edison/projgeo3Copy head branch name to clipboard