Analysis.Section_2

source

@[reducible, inline]

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

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

source

@[implicit_reducible]

instance Chapter2.Nat.instMul :

Mul Nat

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

Equations

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

source

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

source

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

source

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

1 * m = 0 + m

source

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

1 * m = m

Compare with Mathlib's Nat.one_mul

source

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

2 * m = 0 + m + m

source

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

source

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

source

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

source

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

m * 1 = m

Compare with Mathlib's Nat.mul_one

source

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

source

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.

source

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

source

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

source

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

source

@[implicit_reducible]

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.

source

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

source

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)

source

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

source

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)

source

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

source

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.

source

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

source

@[reducible, inline]

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

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

source

@[implicit_reducible]

instance Chapter2.Nat.instPow :

HomogeneousPow Nat

Equations

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

source

@[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

source

@[simp]

theorem Chapter2.Nat.zero_pow_zero :

0 ^ 0 = 1

Definition 2.3.11 (Exponentiation for natural numbers)

source

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

source

@[simp]

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

m ^ 1 = m

Compare with Mathlib's Nat.pow_one

source

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

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

Exercise 2.3.4

Documentation

Analysis.Section_2_3