Documentation

Analysis.Section_2_3

Аналіз I, Розділ 2.3: Множення #

Цей файл є перекладом Глави 2.3 Аналізу I до Lean 4. Вся нумерація посилається на оригінальний текст.

Я (пр.перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним рішенням Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підбуцнути", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Основні конструкції та результати цього розділу:

Визначення множення та піднесення до степеня для натуральних чисел з "Розділу 2". Chapter2.Nat.

Примітка: наприкінці цього розділу клас Chapter2.Nat буде замінено на користь стандартного класу Mathlib _root_.Nat, або ℕ. Однак, ми пропрацюємо властивості Chapter2.Nat "вручну" в наступних кількох розділах для педагогічних цілей.

Підказки від попередніх користувачів #

Користувачі супровідного матеріалу, які виконали вправи в цьому розділі, можуть надсилати свої поради майбутнім користувачам цього розділу як PRи.

(Додайте підказку тут)

@[reducible, inline]

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

Визначення 2.3.1 (Множення натуральних чисел)

Equations

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

Instances For

instance Chapter2.Nat.instMul :

Цей інстанс дозволяє використовувати позначення * для множення натуральних чисел.

Equations

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

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

0 * m = 0

Визначення 2.3.1 (Множення натуральних чисел) Порівняйте із Mathlib-івської Nat.zero_mul

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

n++ * m = n * m + m

Визначення 2.3.1 (Множення натуральних чисел) Порівняйте із Mathlib-івської Nat.succ_mul

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

1 * m = 0 + m

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

1 * m = m

Порівняйте із Mathlib-овським 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

Ця лема буде корисною для доведення Леми 2.3.2. Порівняйте із Mathlib-івської Nat.mul_zero

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

n * m++ = n * m + n

Ця лема буде корисною для доведення Леми 2.3.2. Порівняйте із Mathlib-івської Nat.mul_succ

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

n * m = m * n

Лема 2.3.2 (Множення комутативне) / Вправа 2.3.1 Порівняйте із Mathlib-івської Nat.mul_comm

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

m * 1 = m

Порівняйте із Mathlib-овським Nat.mul_one

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

(n * m).IsPos

Ця лема буде корисною для доведення Леми 2.3.3. Порівняйте із Mathlib-овським Nat.mul_pos

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

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

Лема 2.3.3 (Додатні натуральні числа не мають нульових дільників.) / Вправа 2.3.2. Порівняйте із Mathlib-овським Nat.mul_eq_zero.

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

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

Твердження 2.3.4 (Дістрібутивність) Порівняйте із Mathlib-івської Nat.mul_add

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

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

Твердження 2.3.4 (Дістрібутивність) Порівняйте із Mathlib-івської Nat.add_mul

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

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

Твердження 2.3.5 (Множення асоціативне) / Вправа 2.3.3 Порівняйте із Mathlib-івської Nat.mul_assoc

instance Chapter2.Nat.instCommSemiring :

CommSemiring Nat

(Не в підручнику) Nat є комутативним півкільцем. Це дозволяє застосовувати такі тактики, як ring, до натуральних чисел Розділу 2.

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

Твердження 2.3.6 (Множення зберігає порядок) Порівняйте із Mathlib-івським 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

Твердження 2.3.6 (Множення зберігає порядок)

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

c * a < c * b

Твердження 2.3.6 (Множення зберігає порядок) Порівняйте із Mathlib-івським 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

Твердження 2.3.6 (Множення зберігає порядок)

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

a = b

Наслідок 2.3.7 (Властивість скорочення) Порівняйте із Mathlib-овським Nat.mul_right_cancel

instance Chapter2.Nat.isOrderedRing :

IsOrderedRing Nat

(Не в підручнику) Nat є впорядкованим півкільцем. Це дозволяє застосовувати такі тактики, як gcongr, до натуральних чисел Розділу 2.

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

Твердження 2.3.9 (Лема про ділення Евкліда) / Вправа 2.3.5 Порівняйте із Mathlib-івським Nat.mod_eq_iff

@[reducible, inline]

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

Визначення 2.3.11 (Піднесення до степеня для натуральних чисел)

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

Визначення 2.3.11 (Піднесення до степеня для натуральних чисел) Порівняйте із Mathlib-івським Nat.pow_zero

@[simp]

theorem Chapter2.Nat.zero_pow_zero :

0 ^ 0 = 1

Визначення 2.3.11 (Піднесення до степеня для натуральних чисел)

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

m ^ n++ = m ^ n * m

Визначення 2.3.11 (Піднесення до степеня для натуральних чисел) Порівняйте із Mathlib-івським Nat.pow_succ

@[simp]

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

m ^ 1 = m

Порівняйте із Mathlib-івським Nat.pow_one

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

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

Вправа 2.3.4