From 5c8806ee4183890d41f06827b68fdb399d61b5fd Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 20 May 2024 23:36:31 +0200
Subject: [PATCH 01/15] Update Basic.lean

---
 HepLean/AnomalyCancellation/Basic.lean | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/HepLean/AnomalyCancellation/Basic.lean b/HepLean/AnomalyCancellation/Basic.lean
index 651118c..c609025 100644
--- a/HepLean/AnomalyCancellation/Basic.lean
+++ b/HepLean/AnomalyCancellation/Basic.lean
@@ -16,7 +16,7 @@ It defines a module structure on the charges, and the solutions to the linear AC
 ## TODO
 
 - Derive ACC systems from gauge algebras and fermionic representations.
-- Relate ACCSystems to algebraic varities.
+- Relate ACCSystems to algebraic varieties.
 
 -/
 
@@ -86,7 +86,7 @@ lemma LinSols.ext {χ : ACCSystemLinear} {S T : χ.LinSols} (h : S.val = T.val)
   cases' S
   simp_all only
 
-/-- An instance providng the operations and properties for `LinSols` to form an
+/-- An instance providing the operations and properties for `LinSols` to form an
   addative commutative monoid. -/
 @[simps!]
 instance linSolsAddCommMonoid (χ : ACCSystemLinear) :
@@ -121,7 +121,7 @@ instance linSolsAddCommMonoid (χ : ACCSystemLinear) :
     apply LinSols.ext
     exact χ.chargesAddCommMonoid.nsmul_succ _ _
 
-/-- An instance providng the operations and properties for `LinSols` to form an
+/-- An instance providing the operations and properties for `LinSols` to form an
   module over `ℚ`. -/
 @[simps!]
 instance linSolsModule  (χ : ACCSystemLinear) : Module ℚ χ.LinSols where
@@ -149,7 +149,7 @@ instance linSolsModule  (χ : ACCSystemLinear) : Module ℚ χ.LinSols where
     exact χ.chargesModule.add_smul _ _ _
 
 /-- An instance providing the operations and properties for `LinSols` to form an
-  an addative community. -/
+  an additive community. -/
 instance linSolsAddCommGroup (χ : ACCSystemLinear) : AddCommGroup χ.LinSols :=
   Module.addCommMonoidToAddCommGroup ℚ
 
@@ -271,7 +271,7 @@ structure Hom (χ η : ACCSystem) where
   charges : χ.charges →ₗ[ℚ] η.charges
   /-- The map between solutions. -/
   anomalyFree : χ.Sols → η.Sols
-  /-- The condition that the map commutes with the relevent inclusions. -/
+  /-- The condition that the map commutes with the relevant inclusions. -/
   commute : charges ∘ χ.solsIncl = η.solsIncl ∘ anomalyFree
 
 /-- The definition of composition between two ACCSystems. -/

From 90527e78729f6dbb06416115aaea1eefb2a8e4b8 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 20 May 2024 23:36:36 +0200
Subject: [PATCH 02/15] Update GroupActions.lean

---
 HepLean/AnomalyCancellation/GroupActions.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/HepLean/AnomalyCancellation/GroupActions.lean b/HepLean/AnomalyCancellation/GroupActions.lean
index e9b735b..33bae35 100644
--- a/HepLean/AnomalyCancellation/GroupActions.lean
+++ b/HepLean/AnomalyCancellation/GroupActions.lean
@@ -13,7 +13,7 @@ under which the anomaly equations are invariant.
 
 From this we define
 - The representation acting on the vector space of solutions to the linear ACCs.
-- The group action acting on solutions to the linera + quadratic equations.
+- The group action acting on solutions to the linear + quadratic equations.
 - The group action acting on solutions to the anomaly cancellation conditions.
 
 -/

From 4a129f1e9d1423d23dd78b75bfa1692e097a31bb Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 20 May 2024 23:36:38 +0200
Subject: [PATCH 03/15] Update CliffordAlgebra.lean

---
 HepLean/SpaceTime/CliffordAlgebra.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/HepLean/SpaceTime/CliffordAlgebra.lean b/HepLean/SpaceTime/CliffordAlgebra.lean
index 39dad9b..68b6114 100644
--- a/HepLean/SpaceTime/CliffordAlgebra.lean
+++ b/HepLean/SpaceTime/CliffordAlgebra.lean
@@ -11,8 +11,8 @@ This file defines the Gamma matrices.
 
 ## TODO
 
-- Prove that the algebra generated by the gamma matrices is ismorphic to the
-  Clifford algebra assocaited with spacetime.
+- Prove that the algebra generated by the gamma matrices is isomorphic to the
+  Clifford algebra associated with spacetime.
 - Include relations for gamma matrices.
 -/
 

From 7088bfef3dc91c2cf99f597382cbeb54c85461e5 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 20 May 2024 23:36:41 +0200
Subject: [PATCH 04/15] Update Basic.lean

---
 HepLean/SpaceTime/LorentzGroup/Basic.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/HepLean/SpaceTime/LorentzGroup/Basic.lean b/HepLean/SpaceTime/LorentzGroup/Basic.lean
index 2c2d119..607e063 100644
--- a/HepLean/SpaceTime/LorentzGroup/Basic.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Basic.lean
@@ -113,7 +113,7 @@ def lorentzGroup : Subgroup (GL (Fin 4) ℝ) where
 instance : TopologicalGroup lorentzGroup :=
   Subgroup.instTopologicalGroupSubtypeMem lorentzGroup
 
-/-- The lift of a matrix perserving `ηLin` to a Lorentz Group element. -/
+/-- The lift of a matrix preserving `ηLin` to a Lorentz Group element. -/
 def PreservesηLin.liftLor {Λ : Matrix (Fin 4) (Fin 4) ℝ} (h : PreservesηLin Λ) :
     lorentzGroup := ⟨liftGL h, h⟩
 
@@ -127,24 +127,24 @@ def transpose (Λ : lorentzGroup) : lorentzGroup :=
   PreservesηLin.liftLor ((PreservesηLin.iff_transpose Λ.1).mp Λ.2)
 
 
-/-- The continuous map from `GL (Fin 4) ℝ` to `Matrix (Fin 4) (Fin 4) ℝ` whose kernal is
+/-- The continuous map from `GL (Fin 4) ℝ` to `Matrix (Fin 4) (Fin 4) ℝ` whose kernel is
 the Lorentz group. -/
-def kernalMap : C(GL (Fin 4) ℝ, Matrix (Fin 4) (Fin 4) ℝ) where
+def kernelMap : C(GL (Fin 4) ℝ, Matrix (Fin 4) (Fin 4) ℝ) where
   toFun Λ := η * Λ.1ᵀ * η * Λ.1
   continuous_toFun := by
     apply Continuous.mul _ Units.continuous_val
     apply Continuous.mul _ continuous_const
     exact Continuous.mul continuous_const (Continuous.matrix_transpose (Units.continuous_val))
 
-lemma kernalMap_kernal_eq_lorentzGroup : lorentzGroup = kernalMap ⁻¹' {1} := by
+lemma kernelMap_kernel_eq_lorentzGroup : lorentzGroup = kernelMap ⁻¹' {1} := by
   ext Λ
   erw [mem_iff Λ, PreservesηLin.iff_matrix]
   rfl
 
 /-- The Lorentz Group is a closed subset of `GL (Fin 4) ℝ`. -/
 theorem isClosed_of_GL4 : IsClosed (lorentzGroup : Set (GL (Fin 4) ℝ)) := by
-  rw [kernalMap_kernal_eq_lorentzGroup]
-  exact continuous_iff_isClosed.mp kernalMap.2 {1} isClosed_singleton
+  rw [kernelMap_kernel_eq_lorentzGroup]
+  exact continuous_iff_isClosed.mp kernelMap.2 {1} isClosed_singleton
 
 end lorentzGroup
 

From 503fd417122d10ff2e294ea215319aa0ebc1677f Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 20 May 2024 23:36:45 +0200
Subject: [PATCH 05/15] Update Orthochronous.lean

---
 HepLean/SpaceTime/LorentzGroup/Orthochronous.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
index 832953f..dc0349b 100644
--- a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
@@ -112,7 +112,7 @@ lemma orthchroMapReal_minus_one_or_one (Λ : lorentzGroup) :
 
 local notation  "ℤ₂" => Multiplicative (ZMod 2)
 
-/-- A continuous map from `lorentzGroup` to `ℤ₂` whose kernal are the Orthochronous elements. -/
+/-- A continuous map from `lorentzGroup` to `ℤ₂` whose kernel are the Orthochronous elements. -/
 def orthchroMap : C(lorentzGroup, ℤ₂) :=
   ContinuousMap.comp coeForℤ₂ {
     toFun := fun Λ => ⟨orthchroMapReal Λ, orthchroMapReal_minus_one_or_one Λ⟩,
@@ -169,7 +169,7 @@ lemma mul_not_othchron_of_not_othchron_othchron {Λ Λ' : lorentzGroup} (h : ¬
   rw [zero_zero_mul]
   exact euclid_norm_not_IsFourVelocity_IsFourVelocity h h'
 
-/-- The representation from `lorentzGroup` to `ℤ₂` whose kernal are the Orthochronous elements. -/
+/-- The representation from `lorentzGroup` to `ℤ₂` whose kernel are the Orthochronous elements. -/
 def orthchroRep : lorentzGroup →* ℤ₂ where
   toFun := orthchroMap
   map_one' := by

From 665289854a3e965cabb9e1bafa13c3cee11baf2f Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 20 May 2024 23:36:47 +0200
Subject: [PATCH 06/15] Update TargetSpace.lean

---
 HepLean/StandardModel/HiggsBoson/TargetSpace.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/HepLean/StandardModel/HiggsBoson/TargetSpace.lean b/HepLean/StandardModel/HiggsBoson/TargetSpace.lean
index 5c41e07..37b7bbd 100644
--- a/HepLean/StandardModel/HiggsBoson/TargetSpace.lean
+++ b/HepLean/StandardModel/HiggsBoson/TargetSpace.lean
@@ -42,7 +42,7 @@ abbrev higgsVec := EuclideanSpace ℂ (Fin 2)
 
 section higgsVec
 
-/-- The continous linear map from the vector space `higgsVec` to `(Fin 2 → ℂ)` acheived by
+/-- The continuous linear map from the vector space `higgsVec` to `(Fin 2 → ℂ)` achieved by
 casting vectors. -/
 def higgsVecToFin2ℂ : higgsVec →L[ℝ] (Fin 2 → ℂ) where
   toFun x := x
@@ -69,7 +69,7 @@ noncomputable def higgsRepUnitary : gaugeGroup →* unitaryGroup (Fin 2) ℂ whe
   map_one' := by
     simp only [Prod.snd_one, _root_.map_one, Prod.fst_one, mul_one]
 
-/-- An orthonomral basis of higgsVec. -/
+/-- An orthonormal basis of higgsVec. -/
 noncomputable def orthonormBasis : OrthonormalBasis (Fin 2) ℂ higgsVec :=
   EuclideanSpace.basisFun (Fin 2) ℂ
 
@@ -306,8 +306,8 @@ lemma IsMinOn_potential_iff_of_μSq_nonpos {μSq : ℝ} (hμSq : μSq ≤ 0) :
     exact potential_eq_bound_IsMinOn_of_μSq_nonpos hLam hμSq φ h
 
 end potentialProp
-/-- Given a Higgs vector, a rotation matrix which puts the fst component of the
-vector to zero, and the snd componenet to a real -/
+/-- Given a Higgs vector, a rotation matrix which puts the first component of the
+vector to zero, and the second component to a real -/
 def rotateMatrix (φ : higgsVec) : Matrix (Fin 2) (Fin 2) ℂ :=
   ![![φ 1 /‖φ‖ , - φ 0 /‖φ‖], ![conj (φ 0) / ‖φ‖ , conj (φ 1) / ‖φ‖] ]
 
@@ -353,8 +353,8 @@ lemma rotateMatrix_specialUnitary {φ : higgsVec} (hφ : φ ≠ 0) :
     (rotateMatrix φ) ∈ specialUnitaryGroup (Fin 2) ℂ :=
   mem_specialUnitaryGroup_iff.mpr ⟨rotateMatrix_unitary hφ, rotateMatrix_det hφ⟩
 
-/-- Given a Higgs vector, an element of the gauge group which puts the fst component of the
-vector to zero, and the snd componenet to a real -/
+/-- Given a Higgs vector, an element of the gauge group which puts the first component of the
+vector to zero, and the second component to a real -/
 def rotateGuageGroup {φ : higgsVec} (hφ : φ ≠ 0) : gaugeGroup :=
     ⟨1, ⟨(rotateMatrix φ), rotateMatrix_specialUnitary hφ⟩, 1⟩
 

From ae2b974669bbe81c7d6d1ed815606f85b41a9619 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Tue, 21 May 2024 14:07:53 +0200
Subject: [PATCH 07/15] Update BasisLinear.lean

---
 HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
index 63b1ee5..f8edd17 100644
--- a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
@@ -10,7 +10,7 @@ import Mathlib.Logic.Equiv.Fin
 /-!
 # Basis of `LinSols` in the even case
 
-We give a basis of `LinSols` in the even case. This basis has the special propoerty
+We give a basis of `LinSols` in the even case. This basis has the special property
 that splits into two planes on which every point is a solution to the ACCs.
 -/
 universe v u

From 940c10ce2821ddf05bb1353a053a27deeb49e0d2 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Tue, 21 May 2024 14:08:19 +0200
Subject: [PATCH 08/15] Update LineInCubic.lean

---
 HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
index db47ec0..f87c0fb 100644
--- a/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
@@ -15,10 +15,10 @@ import Mathlib.Tactic.Polyrith
 # Line In Cubic Even case
 
 We say that a linear solution satisfies the `lineInCubic` property
-if the line through that point and through the two different planes formed by the baisis of
+if the line through that point and through the two different planes formed by the basis of
 `LinSols` lies in the cubic.
 
-We show that for a solution all its permutations satsfiy this property, then there exists
+We show that for a solution all its permutations satisfy this property, then there exists
 a permutation for which it lies in the plane spanned by the first part of the basis.
 
 The main reference for this file is:
@@ -34,7 +34,7 @@ open BigOperators
 variable {n : ℕ}
 open VectorLikeEvenPlane
 
-/-- A  property on `LinSols`, statified if every point on the line between the two planes
+/-- A  property on `LinSols`, satisfied if every point on the line between the two planes
 in the basis through that point is in the cubic. -/
 def lineInCubic (S : (PureU1 (2 * n.succ)).LinSols) : Prop :=
   ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = Pa g f) (a b : ℚ) ,

From 85f7800ef26b2f7f22adec05cfc67fef861a459b Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Tue, 21 May 2024 14:10:51 +0200
Subject: [PATCH 09/15] Update Basic.lean

---
 HepLean/AnomalyCancellation/MSSMNu/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
index 1b8ce7c..6af82cc 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
@@ -34,7 +34,7 @@ def MSSMSpecies : ACCSystemCharges := ACCSystemChargesMk 3
 namespace MSSMCharges
 
 /-- An equivalence between `MSSMCharges.charges` and the space of maps
-`(Fin 18 ⊕ Fin 2 → ℚ)`. The first 18 factors corresponds to the SM fermions, whils the last two
+`(Fin 18 ⊕ Fin 2 → ℚ)`. The first 18 factors corresponds to the SM fermions, while the last two
 are the higgsions. -/
 @[simps!]
 def toSMPlusH : MSSMCharges.charges ≃ (Fin 18 ⊕ Fin 2 → ℚ) :=
@@ -173,7 +173,7 @@ lemma accGrav_ext {S T : MSSMCharges.charges}
   rw [hd, hu]
   rfl
 
-/-- The anomaly cancelation condition for SU(2) anomaly. -/
+/-- The anomaly cancellation condition for SU(2) anomaly. -/
 @[simp]
 def accSU2 : MSSMCharges.charges →ₗ[ℚ] ℚ where
   toFun S := ∑ i, (3 * Q S i + L S i) + Hd S + Hu S

From d7eb122dd97b206baf5e91e423d82b27af21301d Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Tue, 21 May 2024 14:10:53 +0200
Subject: [PATCH 10/15] Update Basic.lean

---
 HepLean/AnomalyCancellation/PureU1/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/HepLean/AnomalyCancellation/PureU1/Basic.lean b/HepLean/AnomalyCancellation/PureU1/Basic.lean
index b9f04a3..8ee66dd 100644
--- a/HepLean/AnomalyCancellation/PureU1/Basic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Basic.lean
@@ -10,7 +10,7 @@ import Mathlib.Algebra.BigOperators.Fin
 /-!
 # Pure U(1) ACC system.
 
-We define the anomaly cancellation conditions for a pure U(1) gague theory with `n` fermions.
+We define the anomaly cancellation conditions for a pure U(1) gauge theory with `n` fermions.
 
 -/
 universe v u

From 720afc70e8525c16b063ce64b63a10a6170e90d1 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Tue, 21 May 2024 14:10:54 +0200
Subject: [PATCH 11/15] Update ConstAbs.lean

---
 HepLean/AnomalyCancellation/PureU1/ConstAbs.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean b/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean
index 1acdccc..c3cacd1 100644
--- a/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean
+++ b/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean
@@ -24,7 +24,7 @@ variable {n : ℕ}
 /-- The condition for two rationals to have the same square (equivalent to same abs). -/
 def constAbsProp : ℚ × ℚ → Prop := fun s => s.1^2 = s.2^2
 
-/-- The condition on a charge assigment `S` to have constant absolute value among charges. -/
+/-- The condition on a charge assignment `S` to have constant absolute value among charges. -/
 @[simp]
 def constAbs (S : (PureU1 n).charges) : Prop := ∀ i j, (S i) ^ 2 = (S j) ^ 2
 
@@ -137,7 +137,7 @@ lemma boundary_accGrav'' (k : Fin n) (hk : boundary S k) :
   rw [boundary_castSucc hS hk, boundary_succ hS hk]
   ring
 
-/-- We say a `S ∈ charges` has a boundry if there exists a `k ∈ Fin n` which is a boundary. -/
+/-- We say a `S ∈ charges` has a boundary if there exists a `k ∈ Fin n` which is a boundary. -/
 @[simp]
 def hasBoundary (S : (PureU1 n.succ).charges) : Prop :=
   ∃ (k : Fin n), boundary S k

From 87183d6e931051dcc2adecf5708ac9796dfa180e Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Tue, 21 May 2024 14:10:56 +0200
Subject: [PATCH 12/15] Update Parameterization.lean

---
 HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean b/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
index fd6a18e..2669b53 100644
--- a/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
@@ -16,7 +16,7 @@ import Mathlib.Tactic.Polyrith
 
 Given maps `g : Fin n.succ → ℚ`,  `f : Fin n → ℚ` and `a : ℚ` we form a solution to the anomaly
 equations. We show that every solution can be got in this way, up to permutation, unless it, up to
-permutaiton, lives in the plane spanned by the firt part of the basis vector.
+permutation, lives in the plane spanned by the first part of the basis vector.
 
 The main reference is:
 
@@ -32,7 +32,7 @@ open BigOperators
 variable {n : ℕ}
 open VectorLikeEvenPlane
 
-/-- Given coefficents `g` of a point in `P` and `f` of a point in `P!`, and a rational, we get a
+/-- Given coefficients `g` of a point in `P` and `f` of a point in `P!`, and a rational, we get a
 rational `a ∈ ℚ`, we get a
 point in `(PureU1 (2 * n.succ)).AnomalyFreeLinear`, which we will later show extends to an anomaly
 free point. -/

From 4528d22dc67a7c8d155fdb9e2983adb8a260cf25 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Tue, 21 May 2024 14:12:53 +0200
Subject: [PATCH 13/15] Update LinearParameterization.lean

---
 .../SM/NoGrav/One/LinearParameterization.lean                   | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
index d34340a..01ae991 100644
--- a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
+++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
@@ -46,7 +46,7 @@ lemma ext {S T : linearParameters} (hQ : S.Q' = T.Q') (hY : S.Y = T.Y) (hE : S.E
   cases' S
   simp_all only
 
-/-- The map from the linear paramaters to elements of `(SMNoGrav 1).charges`. -/
+/-- The map from the linear parameters to elements of `(SMNoGrav 1).charges`. -/
 @[simp]
 def asCharges (S : linearParameters) : (SMNoGrav 1).charges := fun i =>
   match i with

From e29a94d39093c0af9a5b0850e6abe46254f310e1 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Tue, 21 May 2024 14:12:55 +0200
Subject: [PATCH 14/15] Update Lemmas.lean

---
 HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
index 6288867..959a0b1 100644
--- a/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
+++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
@@ -12,7 +12,7 @@ import HepLean.AnomalyCancellation.SM.NoGrav.One.LinearParameterization
 The main result of this file is the conclusion of this paper:
 https://arxiv.org/abs/1907.00514
 
-That eveery solution to the ACCs without gravity satisfies for free the gravitational anomaly.
+That every solution to the ACCs without gravity satisfies for free the gravitational anomaly.
 -/
 
 universe v u

From 64d98066da0a2ee28c5f8470630bc0f8bcec90e9 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Tue, 21 May 2024 14:12:57 +0200
Subject: [PATCH 15/15] Update Basic.lean

---
 HepLean/AnomalyCancellation/SM/NoGrav/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/Basic.lean b/HepLean/AnomalyCancellation/SM/NoGrav/Basic.lean
index bdc1a45..4d33c6d 100644
--- a/HepLean/AnomalyCancellation/SM/NoGrav/Basic.lean
+++ b/HepLean/AnomalyCancellation/SM/NoGrav/Basic.lean
@@ -7,7 +7,7 @@ import HepLean.AnomalyCancellation.SM.Basic
 /-!
 # Anomaly Cancellation in the Standard Model without Gravity
 
-This file defines the system of anaomaly equations for the SM without RHN, and
+This file defines the system of anomaly equations for the SM without RHN, and
 without the gravitational ACC.
 
 -/