Documentation

Analysis.Section_2_3

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.

Note: at the end of this chapter, the Chapter2.Nat class will be deprecated in favor of the standard Mathlib class _root_.Nat, or ℕ. However, we will develop the properties of Chapter2.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)

@[reducible, inline]

abbrev Chapter2.Nat.mul (n m : Nat) :

Definition 2.3.1 (Multiplication of natural numbers)

Equations

n.mul m = Chapter2.Nat.recurse (fun (x prod : Chapter2.Nat) => prod + m) 0 n

Instances For

instance Chapter2.Nat.instMul :

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

Equations

Chapter2.Nat.instMul = { mul := Chapter2.Nat.mul }

theorem Chapter2.Nat.zero_mul (m : Nat) :

0 * m = 0

Definition 2.3.1 (Multiplication of natural numbers) Compare with Mathlib's Nat.zero_mul

theorem Chapter2.Nat.succ_mul (n m : Nat) :

n++ * m = n * m + m

Definition 2.3.1 (Multiplication of natural numbers) Compare with Mathlib's Nat.succ_mul

theorem Chapter2.Nat.one_mul' (m : Nat) :

1 * m = 0 + m

theorem Chapter2.Nat.one_mul (m : Nat) :

1 * m = m

Compare with Mathlib's Nat.one_mul

theorem Chapter2.Nat.two_mul (m : Nat) :

2 * m = 0 + m + m

theorem Chapter2.Nat.mul_zero (n : Nat) :

n * 0 = 0

This lemma will be useful to prove Lemma 2.3.2. Compare with Mathlib's Nat.mul_zero

theorem Chapter2.Nat.mul_succ (n m : Nat) :

n * m++ = n * m + n

This lemma will be useful to prove Lemma 2.3.2. Compare with Mathlib's Nat.mul_succ

theorem Chapter2.Nat.mul_comm (n m : Nat) :

n * m = m * n

Lemma 2.3.2 (Multiplication is commutative) / Exercise 2.3.1 Compare with Mathlib's Nat.mul_comm

theorem Chapter2.Nat.mul_one (m : Nat) :

m * 1 = m

Compare with Mathlib's Nat.mul_one

theorem Chapter2.Nat.pos_mul_pos {n m : Nat} (h₁ : n.IsPos) (h₂ : m.IsPos) :

(n * m).IsPos

This lemma will be useful to prove Lemma 2.3.3. Compare with Mathlib's Nat.mul_pos

theorem Chapter2.Nat.mul_eq_zero (n m : Nat) :

n * m = 0 ↔ n = 0 ∨ m = 0

Lemma 2.3.3 (Positive natural numbers have no zero divisors) / Exercise 2.3.2. Compare with Mathlib's Nat.mul_eq_zero.

theorem Chapter2.Nat.mul_add (a b c : Nat) :

a * (b + c) = a * b + a * c

Proposition 2.3.4 (Distributive law) Compare with Mathlib's Nat.mul_add

theorem Chapter2.Nat.add_mul (a b c : Nat) :

(a + b) * c = a * c + b * c

Proposition 2.3.4 (Distributive law) Compare with Mathlib's Nat.add_mul

theorem Chapter2.Nat.mul_assoc (a b c : Nat) :

a * b * c = a * (b * c)

Proposition 2.3.5 (Multiplication is associative) / Exercise 2.3.3 Compare with Mathlib's Nat.mul_assoc

instance Chapter2.Nat.instCommSemiring :

CommSemiring Nat

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

Equations

One or more equations did not get rendered due to their size.

theorem Chapter2.Nat.mul_lt_mul_of_pos_right {a b c : Nat} (h : a < b) (hc : c.IsPos) :

a * c < b * c

Proposition 2.3.6 (Multiplication preserves order) Compare with Mathlib's Nat.mul_lt_mul_of_pos_right

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

a * c > b * c

Proposition 2.3.6 (Multiplication preserves order)

theorem Chapter2.Nat.mul_lt_mul_of_pos_left {a b c : Nat} (h : a < b) (hc : c.IsPos) :

c * a < c * b

Proposition 2.3.6 (Multiplication preserves order) Compare with Mathlib's Nat.mul_lt_mul_of_pos_left

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

c * a > c * b

Proposition 2.3.6 (Multiplication preserves order)

theorem Chapter2.Nat.mul_cancel_right {a b c : Nat} (h : a * c = b * c) (hc : c.IsPos) :

a = b

Corollary 2.3.7 (Cancellation law) Compare with Mathlib's Nat.mul_right_cancel

instance Chapter2.Nat.isOrderedRing :

IsOrderedRing Nat

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

theorem Chapter2.Nat.exists_div_mod (n : Nat) {q : Nat} (hq : q.IsPos) :

∃ (m : Nat) (r : Nat), 0 ≤ r ∧ r < q ∧ n = m * q + r

Proposition 2.3.9 (Euclid's division lemma) / Exercise 2.3.5 Compare with Mathlib's Nat.mod_eq_iff

@[reducible, inline]

abbrev Chapter2.Nat.pow (m n : Nat) :

Definition 2.3.11 (Exponentiation for natural numbers)

Equations

m.pow n = Chapter2.Nat.recurse (fun (x prod : Chapter2.Nat) => prod * m) 1 n

Instances For

instance Chapter2.Nat.instPow :

HomogeneousPow Nat

Equations

Chapter2.Nat.instPow = { pow := Chapter2.Nat.pow }

@[simp]

theorem Chapter2.Nat.pow_zero (m : Nat) :

m ^ 0 = 1

Definition 2.3.11 (Exponentiation for natural numbers) Compare with Mathlib's Nat.pow_zero

@[simp]

theorem Chapter2.Nat.zero_pow_zero :

0 ^ 0 = 1

Definition 2.3.11 (Exponentiation for natural numbers)

theorem Chapter2.Nat.pow_succ (m n : Nat) :

m ^ n++ = m ^ n * m

Definition 2.3.11 (Exponentiation for natural numbers) Compare with Mathlib's Nat.pow_succ

@[simp]

theorem Chapter2.Nat.pow_one (m : Nat) :

m ^ 1 = m

Compare with Mathlib's Nat.pow_one

theorem Chapter2.Nat.sq_add_eq (a b : Nat) :

(a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2

Exercise 2.3.4