Multiplication

Analysis I, Section 2.3: Multiplication

This file is a translation of Section 2.3 of Analysis I to Lean 4. All numbering refers to the original text.

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

Definition of multiplication and exponentiation for the "Chapter 2" natural numbers, Chapter2.Nat : TypeChapter2.Nat.

Note: at the end of this chapter, the Chapter2.Nat : TypeChapter2.Nat class will be deprecated in favor of the standard Mathlib class Nat : Type_root_.Nat, or ℕ : Typeℕ. However, we will develop the properties of Chapter2.Nat : TypeChapter2.Nat "by hand" for pedagogical purposes.

Tips from past users

Users of the companion who have completed the exercises in this section are welcome to send their tips for future users in this section as PRs.

(Add tip here)

namespace Chapter2

Definition 2.3.1 (Multiplication of natural numbers)

abbrev Nat.mul (n m : Nat) : Nat := Nat.recurse (fun _ prod ↦ prod + m) 0 n

This instance allows for the notation to be used for natural number multiplication.

instance Nat.instMul : Mul Nat where
  mul := mul

Definition 2.3.1 (Multiplication of natural numbers) Compare with Mathlib's Chapter2.Nat.zero_mul (m : Nat) : 0 * m = 0Nat.zero_mul

theorem Nat.zero_mul (m: Nat) : 0 * m = 0 := recurse_zero (fun _ prod ↦ prod+m) _

Definition 2.3.1 (Multiplication of natural numbers) Compare with Mathlib's Chapter2.Nat.succ_mul (n m : Nat) : n++ * m = n * m + mNat.succ_mul

theorem Nat.succ_mul (n m: Nat) : (n++) * m = n * m + m := recurse_succ (fun _ prod ↦ prod+m) _ _

theorem Nat.one_mul' (m: Nat) : 1 * m = 0 + m := bym:Nat⊢ 1 * m = 0 + m
  rw [←zero_succ, succ_mul, zero_mul]All goals completed! 🐙

Compare with Mathlib's Chapter2.Nat.one_mul (m : Nat) : 1 * m = mNat.one_mul

theorem Nat.one_mul (m: Nat) : 1 * m = m := bym:Nat⊢ 1 * m = m
  rw [one_mul', zero_add]All goals completed! 🐙

theorem Nat.two_mul (m: Nat) : 2 * m = 0 + m + m := bym:Nat⊢ 2 * m = 0 + m + m
  rw [←one_succ, succ_mul, one_mul']All goals completed! 🐙

This lemma will be useful to prove Lemma 2.3.2. Compare with Mathlib's Chapter2.Nat.mul_zero (n : Nat) : n * 0 = 0Nat.mul_zero

lemma declaration uses 'sorry'Nat.mul_zero (n: Nat) : n * 0 = 0 := byn:Nat⊢ n * 0 = 0
  sorryAll goals completed! 🐙

This lemma will be useful to prove Lemma 2.3.2. Compare with Mathlib's Chapter2.Nat.mul_succ (n m : Nat) : n * m++ = n * m + nNat.mul_succ

lemma declaration uses 'sorry'Nat.mul_succ (n m:Nat) : n * m++ = n * m + n := byn:Natm:Nat⊢ n * m++ = n * m + n
  sorryAll goals completed! 🐙

Lemma 2.3.2 (Multiplication is commutative) / Exercise 2.3.1 Compare with Mathlib's Chapter2.Nat.mul_comm (n m : Nat) : n * m = m * nNat.mul_comm

lemma declaration uses 'sorry'Nat.mul_comm (n m: Nat) : n * m = m * n := byn:Natm:Nat⊢ n * m = m * n
  sorryAll goals completed! 🐙

Compare with Mathlib's Chapter2.Nat.mul_one (m : Nat) : m * 1 = mNat.mul_one

theorem Nat.mul_one (m: Nat) : m * 1 = m := bym:Nat⊢ m * 1 = m
  rw [mul_comm, one_mul]All goals completed! 🐙

This lemma will be useful to prove Lemma 2.3.3. Compare with Mathlib's Nat.mul_pos {n m : ℕ} (ha : n > 0) (hb : m > 0) : n * m > 0Nat.mul_pos

lemma declaration uses 'sorry'Nat.pos_mul_pos {n m: Nat} (h₁: n.IsPos) (h₂: m.IsPos) : (n * m).IsPos := byn:Natm:Nath₁:n.IsPosh₂:m.IsPos⊢ (n * m).IsPos
  sorryAll goals completed! 🐙

Lemma 2.3.3 (Positive natural numbers have no zero divisors) / Exercise 2.3.2. Compare with Mathlib's Chapter2.Nat.mul_eq_zero (n m : Nat) : n * m = 0 ↔ n = 0 ∨ m = 0Nat.mul_eq_zero.

lemma declaration uses 'sorry'Nat.mul_eq_zero (n m: Nat) : n * m = 0 ↔ n = 0 ∨ m = 0 := byn:Natm:Nat⊢ n * m = 0 ↔ n = 0 ∨ m = 0
  sorryAll goals completed! 🐙

Proposition 2.3.4 (Distributive law) Compare with Mathlib's Chapter2.Nat.mul_add (a b c : Nat) : a * (b + c) = a * b + a * cNat.mul_add

theorem Nat.mul_add (a b c: Nat) : a * (b + c) = a * b + a * c := bya:Natb:Natc:Nat⊢ a * (b + c) = a * b + a * c
  -- This proof is written to follow the structure of the original text.
  revert ca:Natb:Nat⊢ ∀ (c : Nat), a * (b + c) = a * b + a * c; apply inductionhbasea:Natb:Nat⊢ a * (b + 0) = a * b + a * 0hinda:Natb:Nat⊢ ∀ (n : Nat), a * (b + n) = a * b + a * n → a * (b + n++) = a * b + a * n++
  .hbasea:Natb:Nat⊢ a * (b + 0) = a * b + a * 0 rw [add_zero]hbasea:Natb:Nat⊢ a * b = a * b + a * 0
    rw [mul_zero, add_zero]All goals completed! 🐙
  intro c habchinda:Natb:Natc:Nathabc:a * (b + c) = a * b + a * c⊢ a * (b + c++) = a * b + a * c++
  rw [add_succ, mul_succ]hinda:Natb:Natc:Nathabc:a * (b + c) = a * b + a * c⊢ a * (b + c) + a = a * b + a * c++
  rw [mul_succ, ←add_assoc, ←habc]All goals completed! 🐙

Proposition 2.3.4 (Distributive law) Compare with Mathlib's Chapter2.Nat.add_mul (a b c : Nat) : (a + b) * c = a * c + b * cNat.add_mul

theorem Nat.add_mul (a b c: Nat) : (a + b)*c = a*c + b*c := bya:Natb:Natc:Nat⊢ (a + b) * c = a * c + b * c
  simp only [mul_comm, mul_add]All goals completed! 🐙

Proposition 2.3.5 (Multiplication is associative) / Exercise 2.3.3 Compare with Mathlib's Chapter2.Nat.mul_assoc (a b c : Nat) : a * b * c = a * (b * c)Nat.mul_assoc

theorem declaration uses 'sorry'Nat.mul_assoc (a b c: Nat) : (a * b) * c = a * (b * c) := bya:Natb:Natc:Nat⊢ a * b * c = a * (b * c)
  sorryAll goals completed! 🐙

(Not from textbook) Nat is a commutative semiring. This allows tactics such as Unknown identifier `ring`ring to apply to the Chapter 2 natural numbers.

instance Nat.instCommSemiring : CommSemiring Nat where
  left_distrib := mul_add
  right_distrib := add_mul
  zero_mul := zero_mul
  mul_zero := mul_zero
  mul_assoc := mul_assoc
  one_mul := one_mul
  mul_one := mul_one
  mul_comm := mul_comm

This illustration of the Unknown identifier `ring`ring tactic is not from the textbook.

example (a b c d:ℕ) : (a+b)*1*(c+d) = d*b+a*c+c*b+a*d+0 := bya:ℕb:ℕc:ℕd:ℕ⊢ (a + b) * 1 * (c + d) = d * b + a * c + c * b + a * d + 0 ringAll goals completed! 🐙

Proposition 2.3.6 (Multiplication preserves order) Compare with Mathlib's Chapter2.Nat.mul_lt_mul_of_pos_right {a b c : Nat} (h : a < b) (hc : c.IsPos) : a * c < b * cNat.mul_lt_mul_of_pos_right

theorem Nat.mul_lt_mul_of_pos_right {a b c: Nat} (h: a < b) (hc: c.IsPos) : a * c < b * c := bya:Natb:Natc:Nath:a < bhc:c.IsPos⊢ a * c < b * c
  -- This proof is written to follow the structure of the original text.
  rw [lt_iff_add_pos] at ha:Natb:Natc:Nath:∃ d, d.IsPos ∧ b = a + dhc:c.IsPos⊢ a * c < b * c
  choose d hdpos hd using ha:Natb:Natc:Nathc:c.IsPosd:Nathdpos:d.IsPoshd:b = a + d⊢ a * c < b * c
  replace hd := congr($hd * c)a:Natb:Natc:Nathc:c.IsPosd:Nathdpos:d.IsPoshd:?_mvar.4948 := id (congrArg (fun x => x * _fvar.4891) _fvar.4944)⊢ a * c < b * c
  rw [add_mul] at hda:Natb:Natc:Nathc:c.IsPosd:Nathdpos:d.IsPoshd:b * c = a * c + d * c⊢ a * c < b * c
  have hdcpos : (d * c).IsPos := pos_mul_pos hdpos hca:Natb:Natc:Nathc:c.IsPosd:Nathdpos:d.IsPoshd:b * c = a * c + d * chdcpos:Chapter2.Nat.IsPos (_fvar.4931 * _fvar.4891) := Chapter2.Nat.pos_mul_pos _fvar.4940 _fvar.4916⊢ a * c < b * c
  rw [lt_iff_add_pos]a:Natb:Natc:Nathc:c.IsPosd:Nathdpos:d.IsPoshd:b * c = a * c + d * chdcpos:Chapter2.Nat.IsPos (_fvar.4931 * _fvar.4891) := Chapter2.Nat.pos_mul_pos _fvar.4940 _fvar.4916⊢ ∃ d, d.IsPos ∧ b * c = a * c + d
  use d*cAll goals completed! 🐙

Proposition 2.3.6 (Multiplication preserves order)

theorem Nat.mul_gt_mul_of_pos_right {a b c: Nat} (h: a > b) (hc: c.IsPos) :
    a * c > b * c := mul_lt_mul_of_pos_right h hc

Proposition 2.3.6 (Multiplication preserves order) Compare with Mathlib's Chapter2.Nat.mul_lt_mul_of_pos_left {a b c : Nat} (h : a < b) (hc : c.IsPos) : c * a < c * bNat.mul_lt_mul_of_pos_left

theorem Nat.mul_lt_mul_of_pos_left {a b c: Nat} (h: a < b) (hc: c.IsPos) : c * a < c * b := bya:Natb:Natc:Nath:a < bhc:c.IsPos⊢ c * a < c * b
  simp [mul_comm]a:Natb:Natc:Nath:a < bhc:c.IsPos⊢ a * c < b * c
  exact mul_lt_mul_of_pos_right h hcAll goals completed! 🐙

Proposition 2.3.6 (Multiplication preserves order)

theorem Nat.mul_gt_mul_of_pos_left {a b c: Nat} (h: a > b) (hc: c.IsPos) :
    c * a > c * b := mul_lt_mul_of_pos_left h hc

Corollary 2.3.7 (Cancellation law) Compare with Mathlib's Nat.mul_right_cancel {n m k : ℕ} (mp : 0 < m) (h : n * m = k * m) : n = kNat.mul_right_cancel

lemma Nat.mul_cancel_right {a b c: Nat} (h: a * c = b * c) (hc: c.IsPos) : a = b := bya:Natb:Natc:Nath:a * c = b * chc:c.IsPos⊢ a = b
  -- This proof is written to follow the structure of the original text.
  have := trichotomous a ba:Natb:Natc:Nath:a * c = b * chc:c.IsPosthis:?_mvar.11884 := Chapter2.Nat.trichotomous _fvar.11877 _fvar.11878⊢ a = b
  obtain hlt | rfl | hgt := thisinla:Natb:Natc:Nath:a * c = b * chc:c.IsPoshlt:a < b⊢ a = binr.inla:Natc:Nathc:c.IsPosh:a * c = a * c⊢ a = ainr.inra:Natb:Natc:Nath:a * c = b * chc:c.IsPoshgt:a > b⊢ a = b
  .inla:Natb:Natc:Nath:a * c = b * chc:c.IsPoshlt:a < b⊢ a = b replace hlt := mul_lt_mul_of_pos_right hlt hcinla:Natb:Natc:Nath:a * c = b * chc:c.IsPoshlt:?_mvar.11956 := Chapter2.Nat.mul_lt_mul_of_pos_right _fvar.11911 _fvar.11881⊢ a = b
    apply ne_of_lt at hltinla:Natb:Natc:Nath:a * c = b * chc:c.IsPoshlt:a * c ≠ b * c⊢ a = b
    contradictionAll goals completed! 🐙
  .inr.inla:Natc:Nathc:c.IsPosh:a * c = a * c⊢ a = a rflAll goals completed! 🐙
  replace hgt := mul_gt_mul_of_pos_right hgt hcinr.inra:Natb:Natc:Nath:a * c = b * chc:c.IsPoshgt:?_mvar.12001 := Chapter2.Nat.mul_gt_mul_of_pos_right _fvar.11939 _fvar.11881⊢ a = b
  apply ne_of_gt at hgtinr.inra:Natb:Natc:Nath:a * c = b * chc:c.IsPoshgt:a * c ≠ b * c⊢ a = b
  contradictionAll goals completed! 🐙

(Not from textbook) Nat is an ordered semiring. This allows tactics such as Unknown identifier `gcongr`gcongr to apply to the Chapter 2 natural numbers.

instance declaration uses 'sorry'Nat.isOrderedRing : IsOrderedRing Nat where
  zero_le_one := by⊢ 0 ≤ 1 sorryAll goals completed! 🐙
  mul_le_mul_of_nonneg_left := by⊢ ∀ (a b c : Nat), a ≤ b → 0 ≤ c → c * a ≤ c * b sorryAll goals completed! 🐙
  mul_le_mul_of_nonneg_right := by⊢ ∀ (a b c : Nat), a ≤ b → 0 ≤ c → a * c ≤ b * c sorryAll goals completed! 🐙

This illustration of the Unknown identifier `gcongr`gcongr tactic is not from the textbook.

example (a b c d:Nat) (hab: a ≤ b) : c*a*d ≤ c*b*d := bya:Natb:Natc:Natd:Nathab:a ≤ b⊢ c * a * d ≤ c * b * d
  gcongra0a:Natb:Natc:Natd:Nathab:a ≤ b⊢ 0 ≤ dh.a0a:Natb:Natc:Natd:Nathab:a ≤ b⊢ 0 ≤ c
  .a0a:Natb:Natc:Natd:Nathab:a ≤ b⊢ 0 ≤ d exact d.zero_leAll goals completed! 🐙
  exact c.zero_leAll goals completed! 🐙

Proposition 2.3.9 (Euclid's division lemma) / Exercise 2.3.5 Compare with Mathlib's Nat.mod_eq_iff {a b c : ℕ} : a % b = c ↔ b = 0 ∧ a = c ∨ c < b ∧ ∃ k, a = b * k + cNat.mod_eq_iff

theorem declaration uses 'sorry'Nat.exists_div_mod (n:Nat) {q: Nat} (hq: q.IsPos) :
    ∃ m r: Nat, 0 ≤ r ∧ r < q ∧ n = m * q + r := byn:Natq:Nathq:q.IsPos⊢ ∃ m r, 0 ≤ r ∧ r < q ∧ n = m * q + r
  sorryAll goals completed! 🐙

Definition 2.3.11 (Exponentiation for natural numbers)

abbrev Nat.pow (m n: Nat) : Nat := Nat.recurse (fun _ prod ↦ prod * m) 1 n

instance Nat.instPow : HomogeneousPow Nat where
  pow := Nat.pow

Definition 2.3.11 (Exponentiation for natural numbers) Compare with Mathlib's Chapter2.Nat.pow_zero (m : Nat) : m ^ 0 = 1Nat.pow_zero

@[simp]
theorem Nat.pow_zero (m: Nat) : m ^ (0:Nat) = 1 := recurse_zero (fun _ prod ↦ prod * m) _

Definition 2.3.11 (Exponentiation for natural numbers)

@[simp]
theorem Nat.zero_pow_zero : (0:Nat) ^ 0 = 1 := recurse_zero (fun _ prod ↦ prod * 0) _

Definition 2.3.11 (Exponentiation for natural numbers) Compare with Mathlib's Chapter2.Nat.pow_succ (m n : Nat) : m ^ n++ = m ^ n * mNat.pow_succ

theorem Nat.pow_succ (m n: Nat) : (m:Nat) ^ n++ = m^n * m :=
  recurse_succ (fun _ prod ↦ prod * m) _ _

Compare with Mathlib's Chapter2.Nat.pow_one (m : Nat) : m ^ 1 = mNat.pow_one

@[simp]
theorem Nat.pow_one (m: Nat) : m ^ (1:Nat) = m := bym:Nat⊢ m ^ 1 = m
  rw [←zero_succ, pow_succ]m:Nat⊢ m ^ 0 * m = m; simpAll goals completed! 🐙

Exercise 2.3.4

theorem declaration uses 'sorry'Nat.sq_add_eq (a b: Nat) :
    (a + b) ^ (2 : Nat) = a ^ (2 : Nat) + 2 * a * b + b ^ (2 : Nat) := bya:Natb:Nat⊢ (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2
  sorryAll goals completed! 🐙

end Chapter2