第5章 初等数论 - 深度伴读
本章定位
本章进入真正的数学内容，核心概念：
- 整除
∣和素数Prime- 互素
Coprime- 归纳法
induction- 强归纳和良序原理
5.1 Irrational Roots
核心思想
证明 √2 是无理数的经典方法：反证法 + 素数性质
关键定义
-- 互素
Nat.Coprime m n = Nat.gcd m n = 1
-- 素数
Nat.Prime p ↔ 2 ≤ p ∧ ∀ m, m < p → m ∣ p → m = 1关键定理
-- 素数整除乘积
Nat.Prime.dvd_mul : Prime p → p ∣ a * b → p ∣ a ∨ p ∣ b
-- 素数整除幂
Nat.Prime.dvd_of_dvd_pow : Prime p → p ∣ a ^ n → p ∣ a
-- 互素的性质
Nat.Coprime.symm : Coprime m n → Coprime n m
Nat.Coprime.dvd_of_dvd_mul_right : Coprime m n → m ∣ n * k → m ∣ k证明 √2 无理数的思路
-- 1. 假设 √2 = m/n（m, n 互素）
-- 2. 平方：m² = 2n²
-- 3. 所以 2 ∣ m²
-- 4. 由素数性质：2 ∣ m
-- 5. 设 m = 2k，则 4k² = 2n²，即 n² = 2k²
-- 6. 所以 2 ∣ n
-- 7. 但这与 m, n 互素矛盾！证明模式
example {m n : ℕ} (coprime_mn : m.Coprime n) : m ^ 2 ≠ 2 * n ^ 2 := by
intro sqr_eq -- 反证法
have : 2 ∣ m := by -- 证明 2 ∣ m
sorry
obtain ⟨k, meq⟩ := ... -- 设 m = 2k
have : 2 ∣ n := by -- 证明 2 ∣ n
sorry
have : 2 ∣ m.gcd n := by -- 2 整除 gcd
sorry
have : 2 ∣ 1 := by -- 矛盾：2 ∣ 1
sorry
norm_num at this -- 关闭目标5.2 Induction and Recursion
核心思想
归纳法是 Lean 中证明自然数性质的主要方法。
归纳法语法
-- 标准归纳法
example (n : ℕ) : P n := by
induction n with
| zero => -- 基础情况：P 0
sorry
| succ n ih => -- 归纳步骤：P n → P (n + 1)
sorry -- ih 是归纳假设强归纳
-- 强归纳：假设对所有 k < n 都成立
example (n : ℕ) : P n := by
induction n using Nat.strong_induction_on with
| _ n ih =>
-- ih : ∀ m, m < n → P m
sorry递归定义
-- 递归函数
def factorial : ℕ → ℕ
| 0 => 1
| n + 1 => (n + 1) * factorial n
-- 用 rec 证明性质
example (n : ℕ) : P n := by
induction n using Nat.rec with
| zero => sorry
| succ n ih => sorryomega 战术
-- omega 自动证明线性算术
example (a b : ℕ) (h1 : a ≤ b) (h2 : b ≤ a) : a = b := by omega
example (a b : ℕ) (h : a + b = 0) : a = 0 ∧ b = 0 := by omega5.3 Infinitely Many Primes
核心思想
Euclid 证明：假设只有有限个素数，构造新素数导出矛盾。
证明思路
-- 1. 假设只有有限个素数 p₁, ..., pₙ
-- 2. 考虑 N = p₁ * p₂ * ... * pₙ + 1
-- 3. N > 1，所以有素因子 p
-- 4. p 整除 N 和 p₁ * ... * pₙ
-- 5. 所以 p 整除 1，矛盾！关键定理
-- 存在大于任意数的素数
Nat.exists_infinite_primes : ∀ n, ∃ p, n ≤ p ∧ Prime p
-- 素数整除阶乘加一
-- 如果 p ≤ n，则 p ∣ n! + 1 → p ∣ 1（矛盾）5.4 More on Induction
核心思想
更多归纳法变体：结构归纳、互归纳等。
结构归纳
-- 对列表的归纳
example (l : List α) : P l := by
induction l with
| nil => sorry
| cons hd tl ih => sorry互归纳
-- 互相递归定义
mutual
def even : ℕ → Bool
| 0 => true
| n + 1 => odd n
def odd : ℕ → Bool
| 0 => false
| n + 1 => even n
end本章核心 Tactic 总结
| Tactic | 用途 | 场景 |
|---|---|---|
induction | 归纳证明 | 自然数、列表 |
omega | 线性算术 | 不等式、等式 |
norm_num | 数值计算 | 具体数值 |
obtain | 解包存在 | 整除、素数 |
rcases | 模式匹配 | 存在、合取 |
contradiction | 找矛盾 | 否定 |
本章练习策略
必做练习
- √2 无理数：理解并完成证明
- 归纳法练习：证明自然数性质
- 素数性质：使用 Prime 的性质
练习技巧
遇到卡住的练习
- 先在纸上写证明草稿
- 用
#check查看定理类型- 用
sorry占位，先搭框架- 查看
solutions/目录
预告：第6章会学到什么
第6章进入离散数学：
- 有限集合
Finset - 有限类型
Fintype - 计数论证
自测问题
induction语法是什么？- 归纳假设
ih的类型是什么？omega能证明什么类型的目标？
伴读文档 - 第5章完