more appropriate lemma tab for implication L10

leanprover-community · Dec 20, 2023 · 09c16e9 · 09c16e9
1 parent ce975ae
commit 09c16e9
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Game/Levels/Implication/L10one_ne_zero.lean b/Game/Levels/Implication/L10one_ne_zero.lean
@@ -3,7 +3,7 @@ World "Implication"
 Level 10
 Title "1 ≠ 0"
 
-LemmaTab "012"
+LemmaTab "Peano"
 
 namespace MyNat