natural-number-game

Solututions to the Natural Number Game

Diffstat

1 file changed, 84 insertions, 0 deletions

diff --git a/power.lean b/power.lean
@@ -0,0 +1,84 @@
+lemma zero_pow_zero : 0 ^ 0 = 1 :=
+begin
+  rw pow_zero,
+  refl,
+end
+
+lemma zero_pow_succ (m : ℕ) : 0 ^ (succ m) = 0 :=
+begin
+  rw pow_succ,
+  rw mul_zero,
+  refl,
+end
+
+lemma pow_one (a : ℕ) : a ^ 1 = a :=
+begin
+  rw one_eq_succ_zero,
+  rw pow_succ,
+  rw pow_zero,
+  rw one_mul,
+  refl,
+end
+
+lemma one_pow (m : ℕ) : 1 ^ m = 1 :=
+begin
+  induction m,
+  rw pow_zero,
+  refl,
+  rw pow_succ,
+  rw m_ih,
+  rw mul_one,
+  refl,
+end
+
+lemma pow_add (a m n : ℕ) : a ^ (m + n) = a ^ m * a ^ n :=
+begin
+  induction n,
+  rw add_zero,
+  rw pow_zero,
+  rw mul_one,
+  refl,
+  rw add_succ,
+  repeat {rw pow_succ},
+  rw ← mul_assoc,
+  rw n_ih,
+  refl,
+end
+
+lemma mul_pow (a b n : ℕ) : (a * b) ^ n = a ^ n * b ^ n :=
+begin
+  induction n,
+  repeat {rw pow_zero},
+  rw mul_one,
+  refl,
+  repeat {rw pow_succ},
+  rw n_ih,
+  simp,
+end
+
+lemma pow_pow (a m n : ℕ) : (a ^ m) ^ n = a ^ (m * n) :=
+begin
+  induction n,
+  rw mul_zero,
+  repeat {rw pow_zero},
+  rw mul_succ,
+  rw pow_add,
+  rw pow_succ,
+  rw n_ih,
+  refl,
+end
+
+lemma add_squared (a b : ℕ) : (a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * a * b :=
+begin
+  rw two_eq_succ_one,
+  rw one_eq_succ_zero,
+  repeat {rw pow_succ},
+  repeat {rw pow_zero},
+  repeat {rw one_mul},
+  repeat {rw succ_mul},
+  rw zero_mul,
+  rw zero_add,
+  rw mul_add,
+  repeat {rw add_mul},
+  simp,
+end