From fb90bad32c5c38268cd69e2aab0fd46be2e25487 Mon Sep 17 00:00:00 2001 From: Yannick Seurin Date: Wed, 12 Jun 2024 14:37:49 +0200 Subject: [PATCH 1/2] typo in L07mul_pow.lean --- Game/Levels/Power/L07mul_pow.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Game/Levels/Power/L07mul_pow.lean b/Game/Levels/Power/L07mul_pow.lean index 40fc07e..c095ba9 100644 --- a/Game/Levels/Power/L07mul_pow.lean +++ b/Game/Levels/Power/L07mul_pow.lean @@ -11,7 +11,7 @@ Introduction The music gets ever more dramatic, as we explore the interplay between exponentiation and multiplication. -If you're having trouble exchanging the right `x * y` +If you're having trouble exchanging the right `a * b` because `rw [mul_comm]` swaps the wrong multiplication, then read the documentation of `rw` for tips on how to fix this. " From 47e143cd67669264276f4d66e00a45427ddcc7b9 Mon Sep 17 00:00:00 2001 From: Yannick Seurin Date: Wed, 12 Jun 2024 14:38:20 +0200 Subject: [PATCH 2/2] Update L08pow_pow.lean --- Game/Levels/Power/L08pow_pow.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Game/Levels/Power/L08pow_pow.lean b/Game/Levels/Power/L08pow_pow.lean index c9278d8..ec94ab3 100644 --- a/Game/Levels/Power/L08pow_pow.lean +++ b/Game/Levels/Power/L08pow_pow.lean @@ -39,7 +39,7 @@ Conclusion The music dies down. Is that it? Course it isn't, you can -clearly see that there are two worlds left. +clearly see that there are two levels left. A passing mathematician says that mathematicians don't have a name for the structure you just constructed. You feel cheated.