From 7515fde40251735fa2b3350183fc1cd07db369df Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 20 May 2024 00:19:30 +0200
Subject: [PATCH] Update FamilyMaps.lean

---
 HepLean/AnomalyCancellation/SM/FamilyMaps.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/HepLean/AnomalyCancellation/SM/FamilyMaps.lean b/HepLean/AnomalyCancellation/SM/FamilyMaps.lean
index 2dc75d6..37c5bae 100644
--- a/HepLean/AnomalyCancellation/SM/FamilyMaps.lean
+++ b/HepLean/AnomalyCancellation/SM/FamilyMaps.lean
@@ -7,7 +7,7 @@ import HepLean.AnomalyCancellation.SM.Basic
 /-!
 # Family maps for the Standard Model ACCs
 
-We define the a series of maps between the charges for different numbers of famlies.
+We define the a series of maps between the charges for different numbers of families.
 
 -/
 
@@ -84,7 +84,7 @@ other charges zero.  -/
 def familyEmbedding (m n : ℕ) : (SMCharges m).charges →ₗ[ℚ] (SMCharges n).charges :=
   chargesMapOfSpeciesMap (speciesEmbed m n)
 
-/-- For species, the embeddding of the `1`-family charges into the `n`-family charges in
+/-- For species, the embedding of the `1`-family charges into the `n`-family charges in
 a universal manor. -/
 @[simps!]
 def speciesFamilyUniversial (n : ℕ) :
@@ -98,7 +98,7 @@ def speciesFamilyUniversial (n : ℕ) :
     simp [HSMul.hSMul]
     --rw [show Rat.cast a = a from rfl]
 
-/-- The embeddding of the `1`-family charges into the `n`-family charges in
+/-- The embedding of the `1`-family charges into the `n`-family charges in
 a universal manor. -/
 def familyUniversal ( n : ℕ) : (SMCharges 1).charges →ₗ[ℚ] (SMCharges n).charges :=
   chargesMapOfSpeciesMap (speciesFamilyUniversial n)