clean mathematics

HepLean/Mathematics/Fin.lean

@@ -352,7 +352,7 @@ lemma finExtractTwo_apply_snd {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) :
   rw [← Equiv.eq_symm_apply]
   simp
 
-/-- Takes two maps `Fin n → Fin n` and returns the equivelance they form. -/
+/-- Takes two maps `Fin n → Fin n` and returns the equivalence they form. -/
 def finMapToEquiv (f1 : Fin n → Fin m) (f2 : Fin m → Fin n)
     (h : ∀ x, f1 (f2 x) = x := by decide)
     (h' : ∀ x, f2 (f1 x) = x := by decide) : Fin n ≃ Fin m where

HepLean/Mathematics/Fin/Involutions.lean

@@ -291,11 +291,11 @@ lemma involutionAddEquiv_isSome_image_zero {n : ℕ} :
 
 ## Equivalences of involutions with no fixed points.
 
-The main aim of thes equivalences is to define `involutionNoFixedZeroEquivProd`.
+The main aim of these equivalences is to define `involutionNoFixedZeroEquivProd`.
 
 -/
 
-/-- Fixed point free involutions of `Fin n.succ` can be seperated based on where they sent
+/-- Fixed point free involutions of `Fin n.succ` can be separated based on where they sent
   `0`. -/
 def involutionNoFixedEquivSum {n : ℕ} :
     {f : Fin n.succ → Fin n.succ // Function.Involutive f
@@ -544,7 +544,7 @@ def involutionNoFixedEquivSumSame {n : ℕ} :
   refine Equiv.trans involutionNoFixedEquivSum ?_
   refine Equiv.sigmaCongrRight involutionNoFixedZeroSetEquiv
 
-/-- Ever fixed-point free involutions of `Fin n.succ.succ` can be decomponsed into a
+/-- Ever fixed-point free involutions of `Fin n.succ.succ` can be decomposed into a
   element of `Fin n.succ` (where `0` is sent) and a fixed-point free involution of
   `Fin n`. -/
 def involutionNoFixedZeroEquivProd {n : ℕ} :

HepLean/Mathematics/PiTensorProduct.lean

@@ -154,7 +154,7 @@ lemma induction_mod_tmul
 # Dependent type version of PiTensorProduct.tmulEquiv
 -/
 
-/-- Given two maps `s1` and `s2` whose targets carry an instance of an addative commutative
+/-- Given two maps `s1` and `s2` whose targets carry an instance of an additive commutative
   monoid, the target of the sum of these two maps also carry an instance thereof. -/
 instance : (i : ι1 ⊕ ι2) → AddCommMonoid ((fun i => Sum.elim s1 s2 i) i) := fun i =>
   match i with

HepLean/Mathematics/SO3/Basic.lean

@@ -57,7 +57,7 @@ lemma subtype_val_eq_toGL : (Subtype.val : SO3 → Matrix (Fin 3) (Fin 3) ℝ) =
     Units.val ∘ toGL.toFun :=
   rfl
 
-/-- The inclusino of `SO(3)` into `GL(3,ℝ)` is an injection. -/
+/-- The inclusion of `SO(3)` into `GL(3,ℝ)` is an injection. -/
 lemma toGL_injective : Function.Injective toGL := by
   refine fun A B h ↦ Subtype.eq ?_
   rw [@Units.ext_iff] at h

HepLean/Mathematics/SchurTriangulation.lean

@@ -17,7 +17,7 @@ closed field, e.g., `ℂ`, is unitarily similar to an upper triangular matrix.
 be decomposed as `A = U * T * star U` where `U` is unitary and `T` is upper triangular.
 - `Matrix.schurTriangulationUnitary` : the unitary matrix `U` as previously stated.
 - `Matrix.schurTriangulation` : the upper triangular matrix `T` as previously stated.
-- Some auxilary definitions are not meant to be used directly, but
+- Some auxiliary definitions are not meant to be used directly, but
 `LinearMap.SchurTriangulationAux.of` contains the main algorithm for the triangulation procedure.
 
 -/
@@ -124,8 +124,8 @@ end
 Given a linear endomorphism `f` on a non-trivial finite-dimensional vector space `E` over an
 algebraically closed field `𝕜`, one can always pick an eigenvalue `μ` of `f` whose corresponding
 eigenspace `V` is non-trivial. Given that `E` is also an inner product space, let `bV` and `bW` be
-othonormal bases for `V` and `Vᗮ` respectively. Then, the collection of vectors in `bV` and `bW`
-forms an othornomal basis `bE` for `E`, as the direct sum of `V` and `Vᗮ` is an internal
+orthonormal bases for `V` and `Vᗮ` respectively. Then, the collection of vectors in `bV` and `bW`
+forms an orthonormal basis `bE` for `E`, as the direct sum of `V` and `Vᗮ` is an internal
 decomposition of `E`. The matrix representation of `f` with respect to `bE` satisfies
 $$
 \sideset{_\mathrm{bE}}{_\mathrm{bE}}{[f]} =