Fix a few typos in chapter 9

MIL/C09_Linear_Algebra/S01_Vector_Spaces.lean

@@ -19,7 +19,7 @@ We will start directly abstract linear algebra, taking place in a vector space o
 However you can find information about matrices in
 :numref:`Section %s <matrices>` which does not logically depend on this abstract theory.
 Mathlib actually deals with a more general version of linear algebra involving the word module,
-but for now we will pretend this is only an excentric spelling habit.
+but for now we will pretend this is only an eccentric spelling habit.
 
 The way to say “let :math:`K` be a field and let :math:`V` be a vector space over :math:`K`”
 (and make them implicit arguments to later results) is:
@@ -39,7 +39,7 @@ Mathematically we want to say that having a :math:`K`-vector space structure
 implies having an additive commutative group structure.
 We could tell this to Lean. But then whenever Lean would need to find such a
 group structure on a type :math:`V`, it would go hunting for vector space
-structures using a *completely unspecified* field :math:`K` that cannot be infered
+structures using a *completely unspecified* field :math:`K` that cannot be inferred
 from :math:`V`.
 This would be very bad for the type class synthesis system.
 
@@ -164,7 +164,7 @@ and ``LinearMap.map_smul`` in terms of the coercion to function.
 This is not yet the end of the story. One also want a version of ``map_add`` that applies to
 any (bundled) map preserving addition, such as additive group morphisms, linear maps, continuous
 linear maps, ``K``-algebra maps etc… This one is ``map_add`` (in the root namespace).
-The intermediate version, ``LinearMap.map_add`` is a bit redudant but allows to use dot notation, which
+The intermediate version, ``LinearMap.map_add`` is a bit redundant but allows to use dot notation, which
 can be nice sometimes. A similar story exists for ``map_smul``, and the general framework
 is explained in :numref:`Chapter %s <hierarchies>`.
 EXAMPLES: -/
@@ -328,4 +328,3 @@ example [Fintype ι] : (⨁ i, V i) ≃ₗ[K] (Π i, V i) :=
 
 end families
 -- QUOTE.
-

MIL/C09_Linear_Algebra/S02_Subspaces.lean

@@ -383,7 +383,7 @@ noncomputable example : (V ⧸ LinearMap.ker φ) ≃ₗ[K] range φ := φ.quotKe
 
 -- QUOTE.
 /- TEXT:
-As an exercise, let us prove the correspondance theorem for subspaces of quotient spaces.
+As an exercise, let us prove the correspondence theorem for subspaces of quotient spaces.
 Mathlib knows a slightly more precise version as ``Submodule.comapMkQRelIso``.
 EXAMPLES: -/
 -- QUOTE:

MIL/C09_Linear_Algebra/S03_Endomorphisms.lean

@@ -15,7 +15,7 @@ An important special case of linear maps are endomorphisms: linear maps from a v
 They are interesting because they form a ``K``-algebra. In particular we can evaluate polynomials
 with coefficients in ``K`` on them, and they can have eigenvalues and eigenvectors.
 
-Mathlib uses the abreviation ``Module.End K V := V →ₗ[K] V`` which is convenient when
+Mathlib uses the abbreviation ``Module.End K V := V →ₗ[K] V`` which is convenient when
 using a lot of these (especially after opening the ``Module`` namespace).
 
 EXAMPLES: -/

MIL/C09_Linear_Algebra/S04_Bases.lean

@@ -46,7 +46,7 @@ section matrices
 /- TEXT:
 It is important to understand that this use of ``#eval`` is interesting only for
 exploration, it is not meant to replace a computer algebra system such as Sage.
-The data representation used here for matrices is *not* computationaly
+The data representation used here for matrices is *not* computationally
 efficient in any way. It uses functions instead of arrays and is optimized for
 proving, not computing.
 The virtual machine used by ``#eval`` is also not optimized for this use.
@@ -209,7 +209,7 @@ example : !![1, 1; 1, 1] * !![1, 1; 1, 1] = !![2, 2; 2, 2] := by
 /- TEXT:
 In order to define matrices as functions without loosing the benefits of ``Matrix``
 for type class synthesis, we can use the equivalence ``Matrix.of`` between functions
-and matrices. This equivalence is secretely defined using ``Equiv.refl``.
+and matrices. This equivalence is secretly defined using ``Equiv.refl``.
 
 For instance we can define Vandermonde matrices corresponding to a vector ``v``.
 EXAMPLES: -/
@@ -311,7 +311,7 @@ example (i : ι) : Finsupp.basisSingleOne i = Finsupp.single i 1 :=
 
 -- QUOTE.
 /- TEXT:
-The story of finitely supported functions is uneeded when the indexing type is finite.
+The story of finitely supported functions is unneeded when the indexing type is finite.
 In this case we can use the simpler ``Pi.basisFun`` which gives a basis of the whole
 ``ι → K``.
 EXAMPLES: -/
@@ -669,12 +669,11 @@ example : Cardinal.lift.{v, u} (.mk ι) = Cardinal.lift.{u, v} (.mk ι') :=
 -- QUOTE.
 /- TEXT:
 We can relate the finite dimensional case to this discussion using the coercion
-from natural numbers to finite cardinals (or more precisly the finite cardinals which live in ``Cardinal.{v}`` where ``v`` is the universe level of ``V``).
+from natural numbers to finite cardinals (or more precisely the finite cardinals which live in ``Cardinal.{v}`` where ``v`` is the universe level of ``V``).
 EXAMPLES: -/
 -- QUOTE:
 
 example [FiniteDimensional K V] :
     (FiniteDimensional.finrank K V : Cardinal) = Module.rank K V :=
   finrank_eq_rank K V
 -- QUOTE.
-