Skip to content

Commit

Permalink
fix quoting in \ne Adv Mult level 6
Browse files Browse the repository at this point in the history
  • Loading branch information
kbuzzard committed Jan 24, 2024
1 parent 4cee0fa commit 2cbb347
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,7 @@ We'll prove it using a new and very useful tactic called `have`.

Statement mul_right_eq_one (x y : ℕ) (h : x * y = 1) : x = 1 := by
Hint (strict := true) "We want to use `le_mul_right`, but we need a hypothesis `x * y ≠ 0`
which we don't have. Yet. Execute `have h2 : x * y ≠ 0` (you can type `≠` with `\ne`).
which we don't have. Yet. Execute `have h2 : x * y ≠ 0` (you can type `≠` with `\\ne`).
You'll be asked to
prove it, and then you'll have a new hypothesis which you can apply
`le_mul_right` to."
Expand Down

0 comments on commit 2cbb347

Please sign in to comment.