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

Remove extra space, that prevent translation

Browse Source
This commit is contained in:
Arnaud
2025-07-11 14:00:36 +02:00
parent 3ced7c7fdb
commit 71e5424a17
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
Game/Levels/AdvMultiplication/L09mul_left_cancel.lean
View File

@@ -40,7 +40,7 @@ Statement mul_left_cancel (a b c : ℕ) (ha : a ≠ 0) (h : a * b = a * c) : b =
· rw [h2]
rfl
· Hint "The inductive hypothesis `hd` is \"For all natural numbers `c`, `a * d = a * c → d = c`\".
You can `apply` it `at` any hypothesis of the form `a * d = a * ?`. "
You can `apply` it `at` any hypothesis of the form `a * d = a * ?`."
Hint (hidden := true) "Split into cases `c = 0` and `c = succ e` with `cases c with e`."
cases c with e
· rw [mul_succ, mul_zero] at h