phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

fix escaping issue

Browse Source
This commit is contained in:
Alexander Bentkamp
2023-03-03 15:58:17 +01:00
parent 3cbb4774f1
commit 86f3e07b27
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
server/testgame/TestGame/Levels/Sum/L03_ArithSum.lean
+1 -1
View File
@@ -73,7 +73,7 @@ Hint (n : ℕ) (hn : 2 * ∑ i : Fin (n + 1), ↑i = n * (n + 1)) :
Hint (n : ℕ) (hn : 2 * ∑ i : Fin (n + 1), ↑i = n * (n + 1)) :
2 * (∑ x : Fin (n + 1), ↑x + (n + 1)) = Nat.succ n * (Nat.succ n + 1) =>
"Um Die Induktionshypothese anzuwenden muss man noch
$$2 \\cdot ((\\sum_{x=0}^n x) + (n + 1)) = 2 \\cdot \\sum_{x=0}^n x + 2 \\cdot (n + 1))$$
$$2 \\cdot ((\\sum_\{x=0}^n x) + (n + 1)) = 2 \\cdot \\sum_\{x=0}^n x + 2 \\cdot (n + 1))$$
umschreiben. Dazu kannst du `mul_add` benützen.
"