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

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

diff --git a/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean b/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
index 8ffd5e8..1c11dca 100644
--- a/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
+++ b/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
@@ -7,7 +7,7 @@ import HepLean.AnomalyCancellation.SMNu.Basic
 /-!
 # Family maps for the Standard Model  for RHN 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.
 
 -/
 
@@ -89,7 +89,7 @@ other charges zero.  -/
 def familyEmbedding (m n : ℕ) : (SMνCharges m).charges →ₗ[ℚ] (SMνCharges 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 : ℕ) :
@@ -103,7 +103,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 : ℕ) : (SMνCharges 1).charges →ₗ[ℚ] (SMνCharges n).charges :=
   chargesMapOfSpeciesMap (speciesFamilyUniversial n)