include a cool cover image

Author: kisonecat

.i18n/en/Game.pot

@@ -1,7 +1,7 @@
 msgid ""
 msgstr "Project-Id-Version: Game v4.7.0\n"
 "Report-Msgid-Bugs-To: \n"
-"POT-Creation-Date: Wed Jun 18 21:45:45 2025\n"
+"POT-Creation-Date: Wed Jun 18 21:52:52 2025\n"
 "Last-Translator: \n"
 "Language-Team: none\n"
 "Language: en\n"
@@ -190,6 +190,18 @@ msgstr ""
 msgid "You have just proved `add_right_cancel`"
 msgstr ""
 
+#: Game.Levels.RingWorld.L04
+msgid "zero times anything"
+msgstr ""
+
+#: Game.Levels.RingWorld.L04
+msgid "Using the axioms, we prove zero times anything vanishes."
+msgstr ""
+
+#: Game.Levels.RingWorld.L04
+msgid "You have just proved `zero_mul`"
+msgstr ""
+
 #: Game.Levels.RingWorld
 msgid "Ring World"
 msgstr ""

Game.lean

@@ -17,7 +17,7 @@ Languages "English"
 CaptionShort "Integer Game"
 CaptionLong "Learn Lean at the Ross Mathematics Program"
 -- Prerequisites "" -- add this if your game depends on other games
--- CoverImage "images/cover.png"
+CoverImage "images/cover.png"
 
 /-! Build the game. Show's warnings if it found a problem with your game. -/
 MakeGame

Game/Levels/AxiomWorld/L02_Multiplication.lean

@@ -1,6 +1,4 @@
 import Game.Metadata
-import Mathlib.Algebra.Ring.Defs
-import Mathlib.Tactic.Use
 
 World "AxiomWorld"
 Level 2
@@ -10,9 +8,7 @@ Title "Multiplication"
 variable {R : Type}
 variable [CommRing R]
 
-Introduction "This text is shown as first message when the level is played.
-You can insert hints in the proof below. They will appear in this side panel
-depending on the proof a user provides."
+Introduction "Now we check some facts about multiplication."
 
 /-- associativity of multiplication in a ring -/
 TheoremDoc mul_assoc as "mul_assoc" in "Ring"
@@ -22,9 +18,7 @@ TheoremDoc mul_comm as "mul_comm" in "Ring"
 
 NewTheorem mul_assoc mul_comm
 
-NewTactic rw
-
 Statement ( a b : R ) : a * b = b * a := by
   rw [mul_comm]
 
-Conclusion "This last message appears if the level is solved."
+Conclusion "Let's put multiplication and addition together."