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

harahu · harahu · commit 433c17180bb3 · 2025-12-10T02:48:23.000Z
Typos found and fixed by Codex.
diff --git a/Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean b/Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean
@@ -12,8 +12,8 @@ public import Mathlib.Algebra.Polynomial.Module.AEval
 /-!
 # Annihilating Ideal
 
-Given a commutative ring `R` and an `R`-algebra `A`
-Every element `a : A` defines
+Given a commutative ring `R` and an `R`-algebra `A`,
+every element `a : A` defines
 an ideal `Polynomial.annIdeal a ⊆ R[X]`.
 Simply put, this is the set of polynomials `p` where
 the polynomial evaluation `p(a)` is 0.
@@ -48,7 +48,7 @@ variable {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
 variable (R) in
 /-- `annIdeal R a` is the *annihilating ideal* of all `p : R[X]` such that `p(a) = 0`.
 
-The informal notation `p(a)` stand for `Polynomial.aeval a p`.
+The informal notation `p(a)` stands for `Polynomial.aeval a p`.
 Again informally, the annihilating ideal of `a` is
 `{ p ∈ R[X] | p(a) = 0 }`. This is an ideal in `R[X]`.
 The formal definition uses the kernel of the aeval map. -/
diff --git a/Mathlib/LinearAlgebra/Basis/Submodule.lean b/Mathlib/LinearAlgebra/Basis/Submodule.lean
@@ -208,7 +208,7 @@ variable {M R : Type*} [Ring R] [Nontrivial R] [IsAddTorsionFree R]
 
 /--
 Let `A` be a subgroup of an additive commutative group `M` that is also an `R`-module.
-Construct a basis of `A` as a `ℤ`-basis from a `R`-basis of `E` that generates `A`.
+Construct a basis of `A` as a `ℤ`-basis from an `R`-basis of `E` that generates `A`.
 -/
 noncomputable def addSubgroupOfClosure (h : A = .closure (Set.range b)) :
     Basis ι ℤ A.toIntSubmodule :=
diff --git a/Mathlib/LinearAlgebra/Dimension/Finite.lean b/Mathlib/LinearAlgebra/Dimension/Finite.lean
@@ -266,7 +266,7 @@ theorem iSupIndep.subtype_ne_bot_le_finrank_aux
     _ = Cardinal.lift.{w} (finrank R M : Cardinal.{v}) := by rw [finrank_eq_rank]
     _ = Cardinal.lift.{v} (finrank R M : Cardinal.{w}) := by simp
 
-/-- If `p` is an independent family of submodules of a `R`-finite module `M`, then the
+/-- If `p` is an independent family of submodules of an `R`-finite module `M`, then the
 number of nontrivial subspaces in the family `p` is finite. -/
 noncomputable def iSupIndep.fintypeNeBotOfFiniteDimensional
     {p : ι → Submodule R M} (hp : iSupIndep p) :
@@ -277,7 +277,7 @@ noncomputable def iSupIndep.fintypeNeBotOfFiniteDimensional
   refine lt_of_le_of_lt hp.subtype_ne_bot_le_finrank_aux ?_
   simp [Cardinal.nat_lt_aleph0]
 
-/-- If `p` is an independent family of submodules of a `R`-finite module `M`, then the
+/-- If `p` is an independent family of submodules of an `R`-finite module `M`, then the
 number of nontrivial subspaces in the family `p` is bounded above by the dimension of `M`.
 
 Note that the `Fintype` hypothesis required here can be provided by
diff --git a/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean b/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
@@ -73,7 +73,7 @@ section exteriorPower
 -- New variables `n` and `M`, to get the correct order of variables in the notation.
 variable (n : ℕ) (M : Type u2) [AddCommGroup M] [Module R M]
 
-/-- Definition of the `n`th exterior power of a `R`-module `N`. We introduce the notation
+/-- Definition of the `n`th exterior power of an `R`-module `N`. We introduce the notation
 `⋀[R]^n M` for `exteriorPower R n M`. -/
 abbrev exteriorPower : Submodule R (ExteriorAlgebra R M) :=
   LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ n
diff --git a/Mathlib/LinearAlgebra/ExteriorPower/Pairing.lean b/Mathlib/LinearAlgebra/ExteriorPower/Pairing.lean
@@ -76,7 +76,7 @@ lemma pairingDual_ιMulti_ιMulti {n : ℕ} (f : (_ : Fin n) → Module.Dual R M
 
 section
 
-/-! If a `R`-module `M` has a family of vectors `x : ι → M` and linear maps `f : ι → M`
+/-! If an `R`-module `M` has a family of vectors `x : ι → M` and linear maps `f : ι → M`
 such that `f i (x j)` is `1` or `0` depending on `i = j` or `i ≠ j`, then if `ι` has
 a linear order, then a similar property regarding `pairingDual R M n`
 applies to the family of vectors indexed
diff --git a/Mathlib/LinearAlgebra/Goursat.lean b/Mathlib/LinearAlgebra/Goursat.lean
@@ -12,8 +12,8 @@ public import Mathlib.LinearAlgebra.Quotient.Basic
 /-!
 # Goursat's lemma for submodules
 
-Let `M, N` be modules over a ring `R`. If `L` is a submodule of `M × N` which projects fully on
-to both factors, then there exist submodules `M' ≤ M` and `N' ≤ N` such that `M' × N' ≤ L` and the
+Let `M, N` be modules over a ring `R`. If `L` is a submodule of `M × N` which projects fully onto
+both factors, then there exist submodules `M' ≤ M` and `N' ≤ N` such that `M' × N' ≤ L` and the
 image of `L` in `(M ⧸ M') × (N ⧸ N')` is the graph of an isomorphism `M ⧸ M' ≃ₗ[R] N ⧸ N'`.
 Equivalently, `L` is equal to the preimage in `M × N` of the graph of this isomorphism
 `M ⧸ M' ≃ₗ[R] N ⧸ N'`.
diff --git a/Mathlib/LinearAlgebra/Lagrange.lean b/Mathlib/LinearAlgebra/Lagrange.lean
@@ -14,9 +14,9 @@ public import Mathlib.RingTheory.Polynomial.Basic
 # Lagrange interpolation
 
 ## Main definitions
-* In everything that follows, `s : Finset ι` is a finite set of indexes, with `v : ι → F` an
-  indexing of the field over some type. We call the image of v on s the interpolation nodes,
-  though strictly unique nodes are only defined when v is injective on s.
+* In everything that follows, `s : Finset ι` is a finite set of indices, with `v : ι → F` an
+  indexing of the field over some type. We call the image of `v` on `s` the interpolation nodes,
+  though strictly unique nodes are only defined when `v` is injective on `s`.
 * `Lagrange.basisDivisor x y`, with `x y : F`. These are the normalised irreducible factors of
   the Lagrange basis polynomials. They evaluate to `1` at `x` and `0` at `y` when `x` and `y`
   are distinct.
diff --git a/Mathlib/LinearAlgebra/LeftExact.lean b/Mathlib/LinearAlgebra/LeftExact.lean
@@ -12,7 +12,7 @@ public import Mathlib.LinearAlgebra.BilinearMap
 # The Left Exactness of Hom
 
 
-If `M1 → M2 → M3 → 0` is an exact sequence of `R`-modules and `N` is a `R`-module,
+If `M1 → M2 → M3 → 0` is an exact sequence of `R`-modules and `N` is an `R`-module,
 then `0 → (M3 →ₗ[R] N) → (M2 →ₗ[R] N) → (M1 →ₗ[R] N)` is exact. In this file, we
 show the exactness at `M2 →ₗ[R] N` (`exact_lcomp_of_exact_of_surjective`);
 the injectivity part is `LinearMap.lcomp_injective_of_surjective` in the file
diff --git a/Mathlib/LinearAlgebra/LinearDisjoint.lean b/Mathlib/LinearAlgebra/LinearDisjoint.lean
@@ -103,7 +103,7 @@ The following is the second equivalent characterization of linear disjointness:
   their span is not `R ^ 2`). In particular, if any two elements in the intersection of `M` and `N`
   are commutative, then the rank of the intersection of `M` and `N` is at most one.
 
-  These results are stated using bundled version (i.e. `a : ↥(M ⊓ N)`). If you want a not bundled
+  These results are stated using a bundled version (i.e. `a : ↥(M ⊓ N)`). If you want a non-bundled
   version (i.e. `a : S` with `ha : a ∈ M ⊓ N`), you may use `LinearIndependent.of_comp` and
   `FinVec.map_eq` (in `Mathlib/Data/Fin/Tuple/Reflection.lean`),
   see the following code snippet:
diff --git a/Mathlib/LinearAlgebra/LinearPMap.lean b/Mathlib/LinearAlgebra/LinearPMap.lean
@@ -23,7 +23,7 @@ We define a `SemilatticeInf` with `OrderBot` instance on this, and define three
 Moreover, we define
 * `LinearPMap.graph` is the graph of the partial linear map viewed as a submodule of `E × F`.
 
-Partially defined maps are currently used in `Mathlib` to prove Hahn-Banach theorem
+Partially defined maps are currently used in `Mathlib` to prove the Hahn-Banach theorem
 and its variations. Namely, `LinearPMap.sSup` implies that every chain of `LinearPMap`s
 is bounded above.
 They are also the basis for the theory of unbounded operators.
diff --git a/Mathlib/LinearAlgebra/Matrix/Gershgorin.lean b/Mathlib/LinearAlgebra/Matrix/Gershgorin.lean
@@ -59,7 +59,7 @@ theorem eigenvalue_mem_ball {μ : K} (hμ : Module.End.HasEigenvalue (Matrix.toL
       _ ≤ ∑ j ∈ Finset.univ.erase i, ‖A i j‖ :=
                 (Finset.sum_le_sum fun j _ => mul_le_of_le_one_right (norm_nonneg _) (h_le j))
 
-/-- If `A` is a row strictly dominant diagonal matrix, then it's determinant is nonzero. -/
+/-- If `A` is a row strictly dominant diagonal matrix, then its determinant is nonzero. -/
 theorem det_ne_zero_of_sum_row_lt_diag (h : ∀ k, ∑ j ∈ Finset.univ.erase k, ‖A k j‖ < ‖A k k‖) :
     A.det ≠ 0 := by
   contrapose! h
@@ -69,7 +69,7 @@ theorem det_ne_zero_of_sum_row_lt_diag (h : ∀ k, ∑ j ∈ Finset.univ.erase k
   rw [Module.End.hasEigenvalue_iff, Module.End.eigenspace_zero, ne_comm]
   exact ne_of_lt (LinearMap.bot_lt_ker_of_det_eq_zero (by rwa [LinearMap.det_toLin']))
 
-/-- If `A` is a column strictly dominant diagonal matrix, then it's determinant is nonzero. -/
+/-- If `A` is a column strictly dominant diagonal matrix, then its determinant is nonzero. -/
 theorem det_ne_zero_of_sum_col_lt_diag (h : ∀ k, ∑ i ∈ Finset.univ.erase k, ‖A i k‖ < ‖A k k‖) :
     A.det ≠ 0 := by
   rw [← Matrix.det_transpose]
diff --git a/Mathlib/LinearAlgebra/Matrix/Irreducible/Defs.lean b/Mathlib/LinearAlgebra/Matrix/Irreducible/Defs.lean
@@ -17,7 +17,7 @@ matrices.
 
 We associate a directed graph (quiver) with a matrix `A`, where an edge `i ⟶ j` exists if and only
 if the entry `A i j` is strictly positive. This allows translating algebraic properties of the
-matrix (like powers) into graph-theoretic properties of its quiver (like theexistence of paths).
+matrix (like powers) into graph-theoretic properties of its quiver (like the existence of paths).
 
 ## Main definitions
 
diff --git a/Mathlib/LinearAlgebra/Multilinear/DirectSum.lean b/Mathlib/LinearAlgebra/Multilinear/DirectSum.lean
@@ -16,7 +16,7 @@ This file describes multilinear maps on direct sums.
 ## Main results
 
 * `MultilinearMap.fromDirectSumEquiv` : If `ι` is a `Fintype`, `κ i` is a family of types
-  indexed by `ι` and we are given a `R`-module `M i j` for every `i : ι` and `j : κ i`, this is
+  indexed by `ι` and we are given an `R`-module `M i j` for every `i : ι` and `j : κ i`, this is
   the linear equivalence between `Π p : (i : ι) → κ i, MultilinearMap R (fun i ↦ M i (p i)) M'` and
   `MultilinearMap R (fun i ↦ ⨁ j : κ i, M i j) M'`.
 -/
diff --git a/Mathlib/LinearAlgebra/Reflection.lean b/Mathlib/LinearAlgebra/Reflection.lean
@@ -21,7 +21,7 @@ public import Mathlib.RingTheory.Polynomial.Chebyshev
 Given an element `x` in a module `M` together with a linear form `f` on `M` such that `f x = 2`, the
 map `y ↦ y - (f y) • x` is an involutive endomorphism of `M`, such that:
  1. the kernel of `f` is fixed,
- 2. the point `x ↦ -x`.
+ 2. the point `x` maps to `-x`.
 
 Such endomorphisms are often called reflections of the module `M`. When `M` carries an inner product
 for which `x` is perpendicular to the kernel of `f`, then (with mild assumptions) the endomorphism
@@ -43,7 +43,7 @@ is characterised by properties 1 and 2 above, and is a linear isometry.
 
 ## TODO
 
-Related definitions of reflection exists elsewhere in the library. These more specialised
+Related definitions of reflection exist elsewhere in the library. These more specialised
 definitions, which require an ambient `InnerProductSpace` structure, are `reflection` (of type
 `LinearIsometryEquiv`) and `EuclideanGeometry.reflection` (of type `AffineIsometryEquiv`). We
 should connect (or unify) these definitions with `Module.reflection` defined here.
diff --git a/Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Basic.lean b/Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Basic.lean
@@ -27,7 +27,7 @@ reduced crystallographic root system. It follows [Geck](Geck2017) quite closely.
 
 ## Alternative approaches
 
-The are at least three ways to construct a Lie algebra from a root system:
+There are at least three ways to construct a Lie algebra from a root system:
 1. As a quotient of a free Lie algebra, using the Serre relations
 2. Directly defining the Lie bracket on $H ⊕ K^∣Φ|$
 3. The Geck construction
diff --git a/Mathlib/LinearAlgebra/SpecialLinearGroup.lean b/Mathlib/LinearAlgebra/SpecialLinearGroup.lean
@@ -17,7 +17,7 @@ public import Mathlib.LinearAlgebra.Charpoly.BaseChange
 If `R` is a commutative ring and `V` is an `R`-module,
 we define `SpecialLinearGroup R V` as the subtype of
 linear equivalences `V ≃ₗ[R] V` with determinant 1.
-When `V` doesn't have a finite basis, the determinant is defined by 1
+When `V` doesn't have a finite basis, the determinant is defined to be 1
 and the definition gives `V ≃ₗ[R] V`.
 The interest of this definition is that `SpecialLinearGroup R V`
 has a group structure. (Starting from linear maps wouldn't have worked.)
@@ -31,7 +31,7 @@ When `V` is free and finite over `R`, we define
 * `SpecialLinearGroup.dualMap`
 * `SpecialLinearGroup.baseChange`
 
-We define `Matrix.SpecialLinearGroup.toLin'_equiv`: the mul equivalence
+We define `Matrix.SpecialLinearGroup.toLin'_equiv`: the multiplicative equivalence
 from `Matrix.SpecialLinearGroup n R` to `SpecialLinearGroup R (n → R)`
 and its variant
 `Matrix.SpecialLinearGroup.toLin_equiv`,
diff --git a/Mathlib/LinearAlgebra/Trace.lean b/Mathlib/LinearAlgebra/Trace.lean
@@ -134,7 +134,7 @@ variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]
 variable (N P : Type*) [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P]
 variable {ι : Type*}
 
-/-- The trace of a linear map correspond to the contraction pairing under the isomorphism
+/-- The trace of a linear map corresponds to the contraction pairing under the isomorphism
 `End(M) ≃ M* ⊗ M` -/
 theorem trace_eq_contract_of_basis [Finite ι] (b : Basis ι R M) :
     LinearMap.trace R M ∘ₗ dualTensorHom R M M = contractLeft R M := by
