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

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

diff --git a/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean b/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
index 3d87877..8ea80f4 100644
--- a/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
+++ b/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
@@ -12,7 +12,7 @@ import Mathlib.RepresentationTheory.Basic
 /-!
 # Line in plane condition
 
-We say a `LinSol` satifies the `line in plane` condition if for all distinct `i1`, `i2`, `i3` in
+We say a `LinSol` satisfies the `line in plane` condition if for all distinct `i1`, `i2`, `i3` in
 `Fin n`, we have
 `S i1 = S i2`  or  `S i1 = - S i2` or  `2 S i3 + S i1 + S i2 = 0`.
 
@@ -21,7 +21,7 @@ The main reference for this material is
 
 - https://arxiv.org/pdf/1912.04804.pdf
 
-We will show that `n ≥ 4` the `line in plane` condition on solutions inplies the
+We will show that `n ≥ 4` the `line in plane` condition on solutions implies the
 `constAbs` condition.
 
 -/