Update L08pow_pow.lean

This commit is contained in:
Yannick Seurin
2024-06-12 14:38:20 +02:00
committed by GitHub
parent fb90bad32c
commit 47e143cd67

View File

@@ -39,7 +39,7 @@ Conclusion
The music dies down. Is that it? The music dies down. Is that it?
Course it isn't, you can 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 A passing mathematician says that mathematicians don't have a name
for the structure you just constructed. You feel cheated. for the structure you just constructed. You feel cheated.