greg/NNG
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

typo #57

Browse Source
This commit is contained in:
Jon Eugster
2024-03-24 12:22:24 +01:00
parent 7a9f61123d
commit 4a55822bbb
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
Game/Levels/Multiplication/L07mul_add.lean
View File

@@ -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.