Description: Define the n-dimensional projective space function. A projective space of dimension 1 is a projective line, and a projective space of dimension 2 is a projective plane. Compare df-ehl . This space is considered n-dimensional because the vector space ( k freeLMod ( 0 ... n ) ) is (n+1)-dimensional and the PrjSp function returns equivalence classes with respect to a linear (1-dimensional) relation. (Contributed by BJ and Steven Nguyen, 29-Apr-2023)