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

Merge pull request #107 from arnbod/small-typo

Browse Source 
Remove extra space, that prevent translation
This commit is contained in:
Jon Eugster
2025-09-23 22:56:36 +02:00
committed by GitHub
parent 3558f5bfb6 71e5424a17
commit a1375414fa
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