natural-number-game

Solututions to the Natural Number Game

NameSizeMode
..
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