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] 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