[Merged by Bors] - feat(LinearAlgebra/Projectivization/Action): add instance of SL(n, F) acting on PF^n#39584

Whysoserioushah wants to merge 8 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

Whysoserioushah:edison/projgeo2Whysoserioushah/mathlib4:edison/projgeo2Copy head branch name to clipboard