final tidy-up with multiplication and power files

leanprover-community · Nov 12, 2023 · 908530e · 908530e
1 parent 372c47e
commit 908530e
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 10 deletions.
diff --git a/Game/MyNat/Multiplication.lean b/Game/MyNat/Multiplication.lean
@@ -12,7 +12,3 @@ axiom mul_zero (a : MyNat) : a * 0 = 0
 
 @[MyNat_decide]
 axiom mul_succ (a b : MyNat) : a * (succ b) = a * b + a
-
--- @[MyNat_decide]
--- theorem toNat_mul (m n : MyNat) : (m * n).toNat = m.toNat * n.toNat := by
---   induction n <;> simp [MyNat_decide, *, Nat.mul_succ];
diff --git a/Game/MyNat/Power.lean b/Game/MyNat/Power.lean
@@ -5,19 +5,14 @@ open MyNat
 
 opaque pow : ℕ → ℕ → ℕ
 
+-- notation `a ^ b` for `pow a b`
 instance : Pow ℕ ℕ where
   pow := pow
 
--- notation a ^ b := pow a b
-
 @[MyNat_decide]
 axiom pow_zero (m : ℕ) : m ^ 0 = 1
 
 @[MyNat_decide]
 axiom pow_succ (m n : ℕ) : m ^ (succ n) = m ^ n * m
 
--- @[MyNat_decide]
--- theorem toNat_pow (m n : MyNat) : (m ^ n).toNat = m.toNat ^ n.toNat := by
---   induction n <;> simp [MyNat_decide, *, Nat.pow_zero, Nat.pow_succ];
-
 end MyNat