natural-number-game
Solututions to the Natural Number Game
Name | Size | Mode | |
.. | |||
power.lean | 1311B | -rw-r--r-- |
01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 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