[Lean] Natural Number Game 3. Multiplication World

Multiplication World에서는 Addition World에서 증명했던 Theorem들과, 곱셈에 관한 기본 Theorem들을 사용하여 곱셈의 교환법칙, 결합법칙, 그리고 분배법칙을 증명하고자 한다.

---

Multiplication World Level 1

Theorem mul_one: For any natural number \(m\), we have \(m \times 1=m\).

theorem mul_one (m : ℕ) : m * 1 = m := by

rw [one_eq_succ_zero]
rw [mul_succ m 0]
rw [mul_zero, zero_add]
rfl

---

Multiplication World Level 2

Theorem zero_mul: For all natural numbers \(m\), we have \(0 \times m=0\).

theorem zero_mul (m : ℕ) : 0 * m = 0 := by

induction m with d hd
rw [mul_zero]
rfl
rw [mul_succ, add_zero]
rw [hd]
rfl

---

Multiplication World Level 3

Theorem succ_mul: For all natural numvers \(a\) and \(b\), we have \((\text{succ} \ a) \times b=a \times b+b\).

theorem succ_mul (a b : ℕ) : succ a * b = a * b + b := by

induction b with d dh
repeat rw [mul_zero]
rw [add_zero]
rfl
repeat rw [mul_succ]
rw [dh]
repeat rw [add_assoc]
repeat rw [add_succ]
rw [add_comm a d]
rfl

---

Multiplication World Level 4

Theorem mul_comm: Multiplication is commutative.

theorem mul_comm (a b : ℕ) : a * b = b * a := by

induction b with d dh
rw [mul_zero, zero_mul]
rfl
rw [mul_succ, succ_mul]
rw [dh]
rfl

---

Multiplication World Level 5

Theorem one_mul: For any natural number \(m\), we have \(1 \times m=m\).

theorem one_mul (m : ℕ): 1 * m = m := by

rw [mul_comm]
rw [mul_one]
rfl

---

Multiplication World Level 6

Theorem two_mul: For any natural number \(m\), we have \(2 \times m=m+m\).

theorem two_mul (m : ℕ): 2 * m = m + m := by

rw [two_eq_succ_one]
rw [succ_mul]
rw [one_mul]
rfl

---

Multiplication World Level 7

Theorem mul_add: Multiplication is distributive over addition on the left. In other words, for all natural numbers \(a\),  \(b\) and \(c\), we have \(a(b+c)=ab+ac\).

theorem mul_add (a b c : ℕ) : a * (b + c) = a * b + a * c := by

induction a with d dh
repeat rw [zero_mul]
rw [add_zero]
rfl
repeat rw [succ_mul]
rw [dh]
repeat rw [← add_assoc]
nth_rewrite 2 [add_right_comm]
rfl

---

Multiplication World Level 8

Theorem add_mul: Multiplication is distributive over addition. In other words, for all natural numbers \(a\),  \(b\) and \(c\), we have \((a+b) \times c=ac+bc\).

theorem add_mul (a b c : ℕ) : (a + b) * c = a * c + b * c := by

rw [mul_comm]
rw [mul_add]
rw [mul_comm c a, mul_comm c b]
rfl

---

Multiplication World Level 9

Theorem mul_assoc: Multiplication is associative. In other words, for all natural numbers \(a\),  \(b\) and \(c\), we have \((ab)c=a(bc)\).

theorem mul_assoc (a b c : ℕ) : (a * b) * c = a * (b * c) := by

induction a with d dh
repeat rw [zero_mul]
rfl
repeat rw [succ_mul]
rw [add_mul]
rw [dh]
rfl