From 908530e97c74a1ee308dceabd3e29ff7ba80ca1f Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sun, 12 Nov 2023 12:47:03 +0000 Subject: [PATCH] final tidy-up with multiplication and power files --- Game/MyNat/Multiplication.lean | 4 ---- Game/MyNat/Power.lean | 7 +------ 2 files changed, 1 insertion(+), 10 deletions(-) diff --git a/Game/MyNat/Multiplication.lean b/Game/MyNat/Multiplication.lean index 3a5992f..6ff858a 100644 --- 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 index 4eed2f0..ebfd15b 100644 --- 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