natural-number-game
Solututions to the Natural Number Game
Name | Size | Mode | |
.. | |||
multiplication.lean | 1493B | -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 85 86 87 88 89 90 91 92 93 94 95 96 97
lemma zero_mul (m : ℕ) : 0 * m = 0 := begin induction m, rw mul_zero, refl, rw mul_succ, rw add_zero, rw m_ih, refl, end lemma mul_one (m : ℕ) : m * 1 = m := begin rw one_eq_succ_zero, rw mul_succ, rw mul_zero, rw zero_add, refl, end lemma one_mul (m : ℕ) : 1 * m = m := begin induction m, rw mul_zero, refl, rw mul_succ, rw m_ih, rw succ_eq_add_one, refl, end lemma mul_add (t a b : ℕ) : t * (a + b) = t * a + t * b := begin induction b, rw mul_zero, repeat {rw add_zero}, rw add_succ, repeat {rw mul_succ}, rw ← add_assoc, rw b_ih, refl, end lemma mul_assoc (a b c : ℕ) : (a * b) * c = a * (b * c) := begin induction c, repeat {rw mul_zero}, repeat {rw mul_succ}, rw mul_add, rw c_ih, refl, end lemma succ_mul (a b : ℕ) : succ a * b = a * b + b := begin induction b, repeat {rw mul_zero}, rw add_zero, refl, repeat {rw mul_succ}, rw b_ih, repeat {rw add_succ}, rw add_right_comm, refl, end lemma add_mul (a b t : ℕ) : (a + b) * t = a * t + b * t := begin induction b, rw zero_mul, repeat {rw add_zero}, rw add_succ, repeat {rw succ_mul}, rw b_ih, rw add_assoc, refl, end lemma mul_comm (a b : ℕ) : a * b = b * a := begin induction b, rw mul_zero, rw zero_mul, refl, rw mul_succ, rw succ_mul, rw b_ih, refl, end lemma mul_left_comm (a b c : ℕ) : a * (b * c) = b * (a * c) := begin rw ← mul_assoc, rw mul_comm a b, rw mul_assoc, refl, end