typo in L07mul_pow.lean

2024-06-12 14:37:49 +02:00
parent 401d973028
commit fb90bad32c
1 changed files with 1 additions and 1 deletions
--- 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.
 "