Skip to content

Commit

Permalink
typo #57
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster committed Mar 24, 2024
1 parent 7a9f611 commit 4a55822
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Game/Levels/Multiplication/L07mul_add.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down

0 comments on commit 4a55822

Please sign in to comment.