05.3 算術基本定理#

本節目標#

• 陳述算術基本定理（唯一分解定理）。
• 認識 Mathlib 中質因數分解的核心 API：Nat.factorization 及其引理。
• 理解存在性（歸納法）與唯一性（Euclid lemma）兩部分的證明架構。
• 實際操作：查詢 \(12\) 的分解、推導除數個數公式。

唯一分解定理的陳述#

定理（算術基本定理）：每個大於 \(1\) 的自然數 \(n\) 都可以寫成

其中 \(p_1 < p_2 < \cdots < p_k\) 是質數、 \(e_i \ge 1\) ，且這種表示法唯一。

例如 \(12 = 2^2 \cdot 3\) ， \(360 = 2^3 \cdot 3^2 \cdot 5\) 。

「唯一」是這條定理的靈魂： \(\mathbb{Z}/6\) 這類沒有唯一分解的環中， 數論會徹底變形（ \(6 = 2 \cdot 3 = \sqrt{2} \cdot \sqrt{2} \cdot \sqrt{3} \cdot \sqrt{3}\) 式的曖昧在 \(\mathbb{Z}[\sqrt{-5}]\) 中真實出現： \(6 = 2 \cdot 3 = (1+\sqrt{-5})(1-\sqrt{-5})\) ）。

Mathlib 的 Nat.factorization#

Mathlib 不用「質數列表」表示分解，而是用一個函數直接讀出指數：

#check (Nat.factorization : ℕ → ℕ →₀ ℕ)
-- Nat.factorization n p = p 在 n 中的指數

Nat.factorization n 是一個「從質數到自然數的有限支撐函數」 （類型 ℕ →₀ ℕ，Finsupp），n.factorization p 就是 \(p\) 的指數 \(e_p\) 。

-- 12 = 2^2 * 3
example : Nat.factorization 12 2 = 2 := by decide
example : Nat.factorization 12 3 = 1 := by decide
example : Nat.factorization 12 5 = 0 := by decide

核心引理一覽：

#check Nat.factorization_mul          -- (m*n).factorization = m.factorization + n.factorization（m, n > 0）
#check Nat.pow_factorization_eq       -- p^(n.factorization p) ∣ n，更大的次方不整除
#check Nat.factorization_dvd_iff      -- m ∣ n ↔ 任意 p 的指數 m 的 ≤ n 的
#check Nat.prime_factorization        -- 對質數 p：p.factorization p = 1
#check Nat.eq_of_factorization_eq     -- 由指數函數相等推出兩數相等

存在性：歸納法#

定理：每個 \(n \ge 2\) 都有質因數；從而不斷拆因數即可完成分解。

歸納架構：

1. \(n\) 是質數：完成（自己就是自己的分解）。
2. \(n = a \cdot b\) 且 \(1 < a, b < n\) ：由歸納假設 \(a, b\) 皆可分解，合併即可。

Mathlib 對應的存在性敘述：

#check Nat.exists_prime_and_dvd
-- 對每個 n ≥ 2，存在質數 p 整除 n

example (n : ℕ) (hn : 2 ≤ n) : ∃ p, Nat.Prime p ∧ p ∣ n := by
  obtain ⟨p, hp, hpd⟩ := Nat.exists_prime_and_dvd hn
  exact ⟨p, hp, hpd⟩

完整的分解存在性在 Mathlib 中體現為： \(n = \prod_p p^{\text{factorization } n \; p}\) ：

#check Nat.prod_pow_factorization_eq_self
-- ∏ p ∈ n.factorization.support, p ^ n.factorization p = n

這條引理正是「乘回來等於原數」的形式化，即存在性與唯一性合起來的成品。

唯一性：Euclid lemma#

唯一性的關鍵是 Euclid lemma：

證明思路：設 \(p \nmid a\) ，則 \(\gcd(p, a) = 1\) （ \(p\) 的因數只有 \(1\) 和 \(p\) ）。 由 Bézout 存在 \(u, v\) 使 \(u p + v a = 1\) ，兩邊乘 \(b\) ： \(u p b + v a b = b\) 。 \(p\) 整除左邊兩項，故 \(p \mid b\) 。

這條引理把「唯一性」化為對因數拆法的歸納：若 \(p_1 \cdots p_k = q_1 \cdots q_l\) ， 則 \(p_1 \mid q_1 \cdots q_l\) ，故 \(p_1\) 等於某個 \(q_i\) ，消去後歸納。

Mathlib 對應：

#check Nat.Prime.dvd_mul         -- p ∣ m * n ↔ p ∣ m ∨ p ∣ n
#check Nat.Prime.dvd_of_dvd_mul_right
#check Nat.Prime.coprime_iff_not_dvd
-- p 質數：¬(p ∣ n) ↔ Coprime p n

example (p a b : ℕ) (hp : Nat.Prime p) (h : p ∣ a * b) : p ∣ a ∨ p ∣ b :=
  hp.dvd_mul.mp h

最終的唯一性由 Nat.eq_of_factorization_eq 給出：兩數的 factorization 函數相等 則兩數相等，配合 Nat.factorization_dvd_iff（整除等價於逐點指數 \(\le\) ）， 唯一分解定理在 Lean 中以「指數函數」的語言完整成立。

示範： \(12 = 2^2 \cdot 3\)#

example : Nat.factorization 12 2 = 2 ∧ Nat.factorization 12 3 = 1 := by
  decide

-- 乘回去驗證
example : 2 ^ 2 * 3 ^ 1 = 12 := by norm_num

-- 12 的質因數恰好是 2 和 3
example (p : ℕ) (hp : Nat.Prime p) : p ∣ 12 ↔ p = 2 ∨ p = 3 := by
  decide

也可以互動查詢：

#eval (Nat.factorization 360 2, Nat.factorization 360 3, Nat.factorization 360 5)
-- (3, 2, 1)   因為 360 = 2^3 * 3^2 * 5

除數個數公式#

若 \(n = p_1^{e_1} \cdots p_k^{e_k}\) ，則 \(n\) 的正因數個數為

原因：每個因數形如 \(p_1^{f_1} \cdots p_k^{f_k}\) ，其中 \(0 \le f_i \le e_i\) ， 各指數獨立選擇 \(e_i + 1\) 種。

例： \(12 = 2^2 \cdot 3^1\) ， \(\tau(12) = 3 \cdot 2 = 6\) 。 實際檢查： \(1, 2, 3, 4, 6, 12\) ，恰六個。✓

-- 12 的所有因數個數確實是 6
example : (Finset.filter (fun d => d ∣ 12) (Finset.Icc 1 12)).card = 6 := by
  decide

-- 一般證明的骨架：因數對應指數向量的選擇
#check Nat.factorization_dvd_iff
#check Nat.dvd_sub'

完整的一般證明需要處理 Finsupp 的組合，此處只用 decide 驗證特例； 練習 4 會引導讀者寫出 \(n = p^e\) 情形的證明。

小結與練習#

本節重點：

• 唯一分解 = 存在性（歸納 + 質因數存在）+ 唯一性（Euclid lemma + 消去歸納）。
• Nat.factorization n p 是「 \(p\) 的指數」；整除 ↔ 逐點指數比較。
• Euclid lemma 在 Mathlib 中是 Nat.Prime.dvd_mul。
• 除數個數 \(\tau(n) = \prod (e_i + 1)\) 來自指數的獨立選擇。

練習：

1. 用 #eval 查 \(n = 60, 99, 128\) 的 factorization，手寫出標準分解式。
2. 證明：Nat.factorization (p ^ e) p = e（提示：Nat.factorization_pow）。
3. 證明：若 Nat.Prime p 且 p ∣ n * n，則 p ∣ n （提示：Nat.Prime.dvd_mul 加上自乘的特例）。
4. 設 \(n = p^e\) （ \(p\) 質數），證明 \(n\) 的因數恰為 \(p^0, \dots, p^e\) ： 即 d ∣ p ^ e ↔ ∃ f, f ≤ e ∧ d = p ^ f（提示：Nat.pow_dvd_pow_iff_le 或 對 d 的 factorization 討論）。
5. 挑戰：用 Nat.factorization_dvd_iff 證明 \(\gcd\) 的指數公式： (Nat.gcd m n).factorization p = min (m.factorization p) (n.factorization p) （提示：Nat.factorization_gcd，先自己嘗試再看內建引理）。