doc(LinearAlgebra): fix typos (leanprover-community#37341)

These typos were found and fixed by Claude Opus 4.6.

Author: harahu

Mathlib/LinearAlgebra/Center.lean

@@ -21,13 +21,13 @@ the center of `Module.End R V`.
 In what follows, `V` is assumed to be a free `R`-module.
 
 * `LinearMap.commute_transvections_iff_of_basis`:
-  if an endomorphism `f : V →ₗ[R] V` commutes with every elementary transvections
-  (in a given basis), then it is an homothety with central ratio.
+  if an endomorphism `f : V →ₗ[R] V` commutes with every elementary transvection
+  (in a given basis), then it is a homothety with central ratio.
   (Assumes that the basis is provided and has a non trivial set of indices.)
 
 * `LinearMap.exists_eq_smul_id_of_forall_notLinearIndependent`:
   over a commutative ring `R` which is a domain, an endomorphism `f : V →ₗ[R] V`
-  of a free domain such that `v` and `f v` are not linearly independent,
+  of a free module such that `v` and `f v` are not linearly independent,
   for all `v : V`, is a homothety.
 
 * `LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent`:
@@ -41,7 +41,7 @@ In what follows, `V` is assumed to be a free `R`-module.
 Note. In the noncommutative case, the last two results do not hold
 when the rank is equal to 1. Indeed, right multiplications
 with noncentral ratio of the `R`-module `R` satisfy the property
-that `f v` and `v` are linearly independent, for all `v : V`,
+that `f v` and `v` are linearly dependent, for all `v : V`,
 but they are not left multiplication by some element.
 
 -/
@@ -92,17 +92,17 @@ theorem commute_transvections_iff_of_basis
 
 set_option backward.isDefEq.respectTransparency false in
 /-- Over a domain, an endomorphism `f` of a free module `V`
-of rank ≠ 1 such that `f v` and `v` are colinear, for all `v : V`,
+of rank ≠ 1 such that `f v` and `v` are collinear, for all `v : V`,
 consists of homotheties with central ratio.
 
 In the commutative case, use `LinearMap.exists_eq_smul_id`.
 
 This is a variant of `LinearMap.exists_mem_center_apply_smul`
-which switches the use `StrongRankInduction` and `finrank`
+which switches the use of `StrongRankInduction` and `finrank`
 for the cardinality of a given basis.
 
 When `finrank R V = 1`, up to a linear equivalence `V ≃ₗ[R] R`,
-then any `f` is *right*-multiplication by some `a : K`,
+then any `f` is *right*-multiplication by some `a : R`,
 but not necessarily *left*-multiplication by an element of the center of `R`. -/
 theorem exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent_of_basis
     [Ring R] [IsDomain R] [AddCommGroup V] [Module R V]
@@ -181,14 +181,14 @@ theorem exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent_of_basis
 
 set_option backward.isDefEq.respectTransparency false in
 /-- Over a domain `R`, an endomorphism `f` of a free module `V`
-of rank ≠ 1 such that `f v` and `v` are colinear, for all `v : V`,
+of rank ≠ 1 such that `f v` and `v` are collinear, for all `v : V`,
 consists of homotheties with central ratio.
 
-When `R`does not satisfy `StrongRankCondition`, use
+When `R` does not satisfy `StrongRankCondition`, use
 `LinearMap.exists_mem_center_apply_eq_smul_of_basis`.
 
 When `finrank R V = 1`, up to a linear equivalence `V ≃ₗ[R] R`,
-then any `f` is *right*-multiplication by some `a : K`,
+then any `f` is *right*-multiplication by some `a : R`,
 but not necessarily *left*-multiplication by an element of the center of `R`. -/
 theorem exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent
     [Ring R] [IsDomain R] [StrongRankCondition R]
@@ -210,7 +210,7 @@ theorem exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent
   exact exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent_of_basis b h
 
 /-- Over a commutative domain, an endomorphism `f` of a free module `V`
-such that `f v` and `v` are colinear, for all `v : V`,
+such that `f v` and `v` are collinear, for all `v : V`,
 consists of homotheties. -/
 theorem exists_eq_smul_id_of_forall_notLinearIndependent
     [CommRing R] [IsDomain R] [AddCommGroup V] [Module R V] [Free R V] {f : V →ₗ[R] V}

Mathlib/LinearAlgebra/JordanChevalley.lean

@@ -17,10 +17,10 @@ sufficient condition for there to exist a nilpotent endomorphism `n` and a semis
 `s`, such that `f = n + s` and both `n` and `s` are polynomial expressions in `f`.
 
 The condition is that there exists a separable polynomial `P` such that the endomorphism `P(f)` is
-nilpotent. This condition is always satisfied when the coefficients are a perfect field.
+nilpotent. This condition is always satisfied when the coefficient field is perfect.
 
 The proof given here uses Newton's method and is taken from Chambert-Loir's notes:
-[Algebre](http://webusers.imj-prg.fr/~antoine.chambert-loir/enseignement/2022-23/agreg/algebre.pdf)
+[Algèbre](http://webusers.imj-prg.fr/~antoine.chambert-loir/enseignement/2022-23/agreg/algebre.pdf)
 
 ## Main definitions / results: