From 4a55822bbb4d52a91ca222f7b045cbe53379be76 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Sun, 24 Mar 2024 12:22:24 +0100
Subject: [PATCH] typo #57

---
 Game/Levels/Multiplication/L07mul_add.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Game/Levels/Multiplication/L07mul_add.lean b/Game/Levels/Multiplication/L07mul_add.lean
index e2db4e7..5303ffe 100644
--- a/Game/Levels/Multiplication/L07mul_add.lean
+++ b/Game/Levels/Multiplication/L07mul_add.lean
@@ -11,7 +11,7 @@ Introduction
 Our next goal is \"left and right distributivity\",
 meaning $a(b+c)=ab+ac$ and $(b+c)a=ba+ca$. Rather than
 these slightly pompous names, the name of the proofs
-of the proof in Lean are descriptive. Let's start with
+in Lean are descriptive. Let's start with
 `mul_add a b c`, the proof of `a * (b + c) = a * b + a * c`.
 Note that the left hand side contains a multiplication
 and then an addition.