chore: fix typos

Author: int-y1

Mathlib/Algebra/Homology/Factorizations/CM5a.lean

@@ -39,7 +39,7 @@ induces a monomorphism in homology in degree `n₁`, and we proceed further
 in `step₂`.
 
 As we assume that both `K` and `L` are bounded below, we may find `n₀ : ℤ`
-such that `K` and `L` are striclty `≥ n₀ + 1`: in particular, `f` induces
+such that `K` and `L` are strictly `≥ n₀ + 1`: in particular, `f` induces
 an isomorphism in degrees `≤ n₀`. Iterating the lemma `step`, we construct
 a projective system `ℕᵒᵖ ⥤ CochainComplex C ℤ`
 (see `CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.cochainComplexFunctor`).

Mathlib/Algebra/Lie/Basis.lean

@@ -145,14 +145,14 @@ private lemma cartan_lie_mem_lieSpan_e {x y : L}
     rw [leibniz_lie, ← lie_skew _ v, neg_add_eq_sub]
     exact sub_mem (LieSubalgebra.lie_mem _ hu hv') (LieSubalgebra.lie_mem _ hv hu')
 
-/-- The nilpotent part of the "upper" Borel subalgebra assocated to a basis. -/
+/-- The nilpotent part of the "upper" Borel subalgebra associated to a basis. -/
 def borelUpper : LieSubmodule R b.cartan L where
   __ := lieSpan R L <| range b.e
   lie_mem {x y} hy := by
     obtain ⟨x, hx⟩ := x
     simpa using b.cartan_lie_mem_lieSpan_e hx hy
 
-/-- The nilpotent part of the "lower" Borel subalgebra assocated to a basis. -/
+/-- The nilpotent part of the "lower" Borel subalgebra associated to a basis. -/
 def borelLower : LieSubmodule R b.cartan L where
   __ := lieSpan R L <| range b.f
   lie_mem := b.symm.borelUpper.lie_mem

Mathlib/Algebra/MonoidAlgebra/Defs.lean

@@ -271,7 +271,7 @@ section
 example : (smulZeroClass (A := ℕ) (R := R) (M := M)).toSMul = addCommMonoid.toNSMul := by
   with_reducible_and_instances rfl
 
--- Enusre that smul has good defeq properties
+-- Ensure that smul has good defeq properties
 private local instance {α} [Monoid M] [SMul M α] : SMul Mˣ α where smul m a := (m : M) • a
 example [Monoid A] [SMulZeroClass A R] (a : Units A) (x : R[M]) :
     a • x = (a : A) • x := by

Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean

@@ -648,7 +648,7 @@ lemma coeff_weierstrassPExceptSeries (l₀ x : ℂ) (i : ℕ) :
 
 /--
 In the power series expansion of `℘(z) = ∑ᵢ aᵢ (z - x)ⁱ` at some `x ∉ L`,
-each `aᵢ` can be writen as a sum over `l ∈ L`, i.e.
+each `aᵢ` can be written as a sum over `l ∈ L`, i.e.
 `aᵢ = ∑ₗ, (i + 1) * (l - x)⁻ⁱ⁻²` for `i ≠ 0` and `a₀ = ∑ₗ, (l - x)⁻² - l⁻²`.
 
 We show that the double sum converges if `z` falls in a ball centered at `x` that doesn't touch `L`.

Mathlib/CategoryTheory/Monoidal/Mon_.lean

@@ -56,7 +56,7 @@ variable {C : Type u₁} [Category.{v₁} C] [MonoidalCategory.{v₁} C]
 class AddMonObj (X : C) where
   /-- The zero morphism of an additive monoid object. -/
   zero : 𝟙_ C ⟶ X
-  /-- The additiion morphism of an additive monoid object. -/
+  /-- The addition morphism of an additive monoid object. -/
   add : X ⊗ X ⟶ X
   zero_add (X) : zero ▷ X ≫ add = (λ_ X).hom := by cat_disch
   add_zero (X) : X ◁ zero ≫ add = (ρ_ X).hom := by cat_disch

Mathlib/CategoryTheory/Retract.lean

@@ -104,7 +104,7 @@ namespace RetractArrow
 
 variable {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g)
 
-set_option backward.isDefEq.respectTransparency false in -- This is needed for MorphismPropert/Retract.lean
+set_option backward.isDefEq.respectTransparency false in -- This is needed for MorphismProperty/Retract.lean
 @[reassoc]
 lemma i_w : h.i.left ≫ g = f ≫ h.i.right := h.i.w
 

Mathlib/CategoryTheory/Triangulated/SpectralObject.lean

@@ -80,7 +80,7 @@ are composable. -/
 def δ : X.ω₁.obj (mk₁ g) ⟶ (X.ω₁.obj (mk₁ f))⟦(1 : ℤ)⟧ :=
   X.δ'.app (mk₂ f g)
 
-/-- The distinguished triangle attached to a spectral object `E : SpectralObjet C ι`
+/-- The distinguished triangle attached to a spectral object `E : SpectralObject C ι`
 and composable morphisms `f : i ⟶ j` and `g : j ⟶ k` in `ι`. -/
 @[simps!]
 def triangle : Triangle C :=

Mathlib/Combinatorics/SimpleGraph/Extremal/TuranDensity.lean

@@ -31,7 +31,7 @@ This file defines the **Turán density** of a simple graph.
   asymptotically equivalent to `turanDensity H * n.choose 2` as `n` approaches `∞`.
 
 * `SimpleGraph.isContained_of_card_edgeFinset`: simple graphs on `n` vertices with at least
-  `(turanDensity H + o(1)) * n ^ 2` edges contain `H`, for all sufficently large `n`.
+  `(turanDensity H + o(1)) * n ^ 2` edges contain `H`, for all sufficiently large `n`.
 -/
 
 @[expose] public section

Mathlib/NumberTheory/Height/MvPolynomial.lean

@@ -36,7 +36,7 @@ variable {R α : Type*} [CommRing R]
 
 -- NOTE: The following cannot be moved to Mathlib.Algebra.Order.Ring.IsNonarchimedean,
 --       because it needs the target to be the reals (to have the default value zero
---       for emtpy iSups), which are not known there.
+--       for empty iSups), which are not known there.
 /-- The ultrametric triangle inequality for finite sums. -/
 lemma apply_sum_le {α β F : Type*} [AddCommMonoid β] [FunLike F β ℝ] [NonnegHomClass F β ℝ]
     [ZeroHomClass F β ℝ] {v : F} (hv : IsNonarchimedean v) {l : α → β} {s : Finset α} :
@@ -392,7 +392,7 @@ If
 * `x : ι → K` is such that for all `k : ι`,
   `∑ j, (q (k, j)).eval x * (p j).eval x = (x k) ^ (M + N)`,
 then the multiplicative height of `fun j ↦ (p j).eval x` is bounded below by an (explicit) positive
-constant depending only on `q` times the `N`th power of the mutiplicative height of `x`.
+constant depending only on `q` times the `N`th power of the multiplicative height of `x`.
 A similar statement holds for the logarithmic height.
 
 Note that we only require the polynomial relations `∑ j, q (k, j) * p j = X k ^ (M + N)`
@@ -429,7 +429,7 @@ open AdmissibleAbsValues
 * `x : ι → K` is such that for all `k : ι`,
   `∑ j, (q (k, j)).eval x * (p j).eval x = (x k) ^ (M + N)`,
 then the multiplicative height of `fun j ↦ (p j).eval x` is bounded below by an (explicit) positive
-constant depending only on `q` times the `N`th power of the mutiplicative height of `x`. -/
+constant depending only on `q` times the `N`th power of the multiplicative height of `x`. -/
 theorem mulHeight_eval_ge {M N : ℕ} {q : ι × ι' → MvPolynomial ι K}
     (hq : ∀ a, (q a).IsHomogeneous M) (p : ι' → MvPolynomial ι K) {x : ι → K}
     (h : ∀ k, ∑ j, (q (k, j)).eval x * (p j).eval x = (x k) ^ (M + N)) :
@@ -459,7 +459,7 @@ theorem mulHeight_eval_ge {M N : ℕ} {q : ι × ι' → MvPolynomial ι K}
 * `x : ι → K` is such that for all `k : ι`,
   `∑ j, (q (k, j)).eval x * (p j).eval x = (x k) ^ (M + N)`,
 then the multiplicative height of `fun j ↦ (p j).eval x` is bounded below by a positive
-constant depending only on `q` times the `N`th power of the mutiplicative height of `x`.
+constant depending only on `q` times the `N`th power of the multiplicative height of `x`.
 
 The difference to `mulHeight_eval_ge` is that the constant is not made explicit. -/
 theorem mulHeight_eval_ge' {M N : ℕ} {q : ι × ι' → MvPolynomial ι K}

Mathlib/RingTheory/AdicCompletion/Completeness.lean

@@ -78,7 +78,7 @@ private lemma ofValEqZeroAux_exists {x : AdicCompletion I M} (h : c = b + a)
   simpa [← LinearMap.mem_range, range_powSMulQuotInclusion] using
     (val_apply_mem_smul_top_iff I (show a ≤ c by lia)).mpr ha
 
-/-- An auxillary lift function used in the definition of `ofValEqZero`.
+/-- An auxiliary lift function used in the definition of `ofValEqZero`.
 Use `ofValEqZero` instead. -/
 def ofValEqZeroAux {x : AdicCompletion I M} (h : c = b + a) (ha : x.val a = 0) :
     ↥(I ^ a • ⊤ : Submodule R M) ⧸ I ^ b • (⊤ : Submodule R ↥(I ^ a • ⊤ : Submodule R M)) :=