fix(LinearAlgebra/Projectivization/Independence): use DivisionRing in…

…stead of Field (#11232)

I need $K$ to be a skew field instead of a field to prove that projectivization of a vector space is a projective geometry stated in proposition 2.1.6 in the book "Modern Projective Geometry" by Claude-Alain Faure and Alfred Frölicher, see p. 27-28. In p.27, just before the proposition, it is noted that "... $K$ is allowed to be a skew field (often called *division ring*)."

Mathlib/LinearAlgebra/Projectivization/Independence.lean

@@ -32,7 +32,7 @@ ambient vector space. Similarly for the definition of dependence.
 
 open scoped LinearAlgebra.Projectivization
 
-variable {ι K V : Type*} [Field K] [AddCommGroup V] [Module K V] {f : ι → ℙ K V}
+variable {ι K V : Type*} [DivisionRing K] [AddCommGroup V] [Module K V] {f : ι → ℙ K V}
 
 namespace Projectivization