doc(FieldTheory): fix typos (#36560)

harahu · harahu · commit 5ccfc604026a · 2026-03-31T09:28:39.000Z
Found by `PyCharm`'s code inspection tool. Fixes were made by Codex.
diff --git a/Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean b/Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean
@@ -226,7 +226,7 @@ theorem sup_toSubalgebra_of_isAlgebraic_right [Algebra.IsAlgebraic K E2] :
     IsAlgebraic.tower_top _ (isAlgebraic_iff.mp (Algebra.IsAlgebraic.isAlgebraic (⟨x, h⟩ : E2)))
   apply_fun Subalgebra.restrictScalars K at this
   rw [← restrictScalars_toSubalgebra, restrictScalars_adjoin] at this
-  -- TODO: rather than using `← coe_type_toSubalgera` here, perhaps we should restate another
+  -- TODO: rather than using `← coe_type_toSubalgebra` here, perhaps we should restate another
   -- version of `Algebra.restrictScalars_adjoin` for intermediate fields?
   simp only [← coe_type_toSubalgebra] at this
   rw [Algebra.restrictScalars_adjoin] at this
diff --git a/Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean b/Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean
@@ -15,11 +15,11 @@ public import Mathlib.FieldTheory.IsAlgClosed.Basic
 ## Main definition
 - `minpolyDiv`: The polynomial `minpoly R x / (X - C x)`.
 
-We used the contents of this file to describe the dual basis of a powerbasis under the trace form.
+We used the contents of this file to describe the dual basis of a power basis under the trace form.
 See `traceForm_dualBasis_powerBasis_eq`.
 
 ## Main results
-- `span_coeff_minpolyDiv`: The coefficients of `minpolyDiv` spans `R<x>`.
+- `span_coeff_minpolyDiv`: The coefficients of `minpolyDiv` span `R<x>`.
 -/
 
 @[expose] public section
diff --git a/Mathlib/FieldTheory/RatFunc/Luroth.lean b/Mathlib/FieldTheory/RatFunc/Luroth.lean
@@ -499,7 +499,7 @@ lemma θ_natDegree_le (h : E ≠ ⊥) : (θ E).natDegree ≤ m E := by
   · rw [natDegree_mul (C_ne_zero.mpr (num_ne_zero (generator_ne_zero h)))
       (Polynomial.map_ne_zero (generator E).denom_ne_zero), natDegree_C, zero_add, natDegree_map]
 
-/-- Equation (11.3.8) from Cohns proof, viewed as an equation of polynomials with coefficients
+/-- Equation (11.3.8) from Cohn's proof, viewed as an equation of polynomials with coefficients
 in `K⟮X⟯`. -/
 lemma Q₀_mul_Φ (h : E ≠ ⊥) :
     Q₀ E * (Φ E).map (algebraMap K[X] K⟮X⟯) = (θ E).map (algebraMap K[X] K⟮X⟯) := by
@@ -536,7 +536,7 @@ lemma Q₁_ne_zero (h : E ≠ ⊥) : Q₁ h ≠ 0 := by
   rw [map_Q₁, Polynomial.map_zero]
   exact Q₀_ne_zero h
 
-/-- Equation (11.3.8) from Cohns proof, viewed as an equation of bivariate polynomials. -/
+/-- Equation (11.3.8) from Cohn's proof, viewed as an equation of bivariate polynomials. -/
 lemma Q₁_mul_Φ (h : E ≠ ⊥) : Q₁ h * Φ E = θ E := by
   apply_fun Polynomial.map (algebraMap K[X] K⟮X⟯) using
     Polynomial.map_injective _ (algebraMap_injective K)
@@ -569,7 +569,7 @@ lemma Q₂_ne_zero (h : E ≠ ⊥) : Q₂ h ≠ 0 := by
   rw [Polynomial.map_zero, Q₂_map]
   exact Q₁_ne_zero h
 
-/-- Equation (11.3.8) from Cohns proof, where we view `Q` as a univariate polynomial. -/
+/-- Equation (11.3.8) from Cohn's proof, where we view `Q` as a univariate polynomial. -/
 lemma Q₂_mul_Φ (h : E ≠ ⊥) : (Q₂ h).map Polynomial.C * Φ E = θ E := by
   rw [Q₂_map h, Q₁_mul_Φ h]
 
@@ -621,7 +621,7 @@ abbrev Q₃ (h : E ≠ ⊥) : K := (Q₂ h).coeff 0
 lemma Q₃_map (h : E ≠ ⊥) : Polynomial.C (Q₃ h) = Q₂ h :=
   (eq_C_of_natDegree_eq_zero (Q₂_natDegree h)).symm
 
-/-- Equation (11.3.8) from Cohns proof, where we view `Q` as a constant. -/
+/-- Equation (11.3.8) from Cohn's proof, where we view `Q` as a constant. -/
 lemma Q₃_mul_Φ (h : E ≠ ⊥) : (Polynomial.C (Q₃ h)).map Polynomial.C * Φ E = θ E := by
   rw [Q₃_map h, Q₂_mul_Φ h]
 
diff --git a/Mathlib/FieldTheory/SeparablyGenerated.lean b/Mathlib/FieldTheory/SeparablyGenerated.lean
@@ -186,11 +186,12 @@ variable [ExpChar k p]
 include hp H
 
 /--
-Suppose `k` has chararcteristic `p` and `a₁,...,aₙ` is a transcendental basis of `K/k`.
+Suppose `k` has characteristic `p` and `a₁,...,aₙ` is a transcendence basis of `K/k`.
 Suppose furthermore that if `{ sᵢ } ⊆ K` is an arbitrary `k`-linearly independent set,
 `{ sᵢᵖ } ⊆ K` is also `k`-linearly independent (which is true when `K ⊗ₖ k^{1/p}` is reduced).
 
-Then some subset of `a₁,...,aₙ₊₁` forms a transcedental basis that `a₁,...,aₙ₊₁` are separable over.
+Then some subset of `a₁,...,aₙ₊₁` forms a transcendence basis over which `a₁,...,aₙ₊₁` are
+separable.
 -/
 lemma exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow
     (ha' : IsTranscendenceBasis k fun i : {i // i ≠ n} ↦ a i) :
@@ -248,12 +249,12 @@ lemma exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow'
   refine ⟨i, hi.comp_equiv e₂.symm, by convert hi'⟩
 
 /--
-Suppose `k` has chararcteristic `p` and `K/k` is generated by `a₁,...,aₙ₊₁`,
-where `a₁,...aₙ` forms a transcendental basis.
+Suppose `k` has characteristic `p` and `K/k` is generated by `a₁,...,aₙ₊₁`,
+where `a₁,...aₙ` form a transcendence basis.
 Suppose furthermore that if `{ sᵢ } ⊆ K` is an arbitrary `k`-linearly independent set,
 `{ sᵢᵖ } ⊆ K` is also `k`-linearly independent (which is true when `K ⊗ₖ k^{1/p}` is reduced).
 
-Then some subset of `a₁,...,aₙ₊₁` forms a separable transcedental basis.
+Then some subset of `a₁,...,aₙ₊₁` forms a separating transcendence basis.
 -/
 @[stacks 0H71]
 lemma exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_adjoin_eq_top
@@ -271,15 +272,15 @@ lemma exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_adjoin
   · exact isSeparable_algebraMap (F := adjoin k (a '' {i}ᶜ)) ⟨_, subset_adjoin _ _ ⟨x, ne, rfl⟩⟩
 
 /--
-Suppose `k` has chararcteristic `p` and `K/k` is finitely generated.
+Suppose `k` has characteristic `p` and `K/k` is finitely generated.
 Suppose furthermore that if `{ sᵢ } ⊆ K` is an arbitrary `k`-linearly independent set,
 `{ sᵢᵖ } ⊆ K` is also `k`-linearly independent (which is true when `K ⊗ₖ k^{1/p}` is reduced).
 
 Then `K/k` is finite separably generated.
 
 TODO: show that this is an if and only if.
 -/
-@[stacks 030W "(2) ⇒ (1) finitely genenerated case"]
+@[stacks 030W "(2) ⇒ (1) finitely generated case"]
 lemma exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_essFiniteType
     [Algebra.EssFiniteType k K] :
     ∃ s : Finset K, IsTranscendenceBasis k ((↑) : s → K) ∧
