Skip to content

Commit

Permalink
Merge pull request #69 from ugur-a/patch-1
Browse files Browse the repository at this point in the history
Fix quoting
  • Loading branch information
joneugster authored Jun 29, 2024
2 parents 3e9657d + 0d828ed commit bfaf125
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions Game/Levels/AdvMultiplication/L09mul_left_cancel.lean
Original file line number Diff line number Diff line change
Expand Up @@ -23,8 +23,8 @@ the hypothesis is `a * d = a * c → d = c` but what we know is `a * succ d = a
so the induction hypothesis does not apply!
Assume `a ≠ 0` is fixed. The actual statement we want to prove by induction on `b` is
\"for all `c`, if `a * b = a * c` then `b = c`. This *can* be proved by induction,
because we now have the flexibility to change `c`.\"
\"for all `c`, if `a * b = a * c` then `b = c`\". This *can* be proved by induction,
because we now have the flexibility to change `c`.
"

Statement mul_left_cancel (a b c : ℕ) (ha : a ≠ 0) (h : a * b = a * c) : b = c := by
Expand Down

0 comments on commit bfaf125

Please sign in to comment.