最大公因數與互質

數學敘述

自然數 d=gcd(a,b) 由 d∣a、d∣b，且每個同時整除 a、b 的自然數 c 都滿足 c∣d 刻畫。採 gcd(0,0)=0；a、b 互質表示 gcd(a,b)=1。

代表公式（精確 TeX）

d=g(a,b)

成立條件

• a、b 是自然數，允許其中一個或兩個為 0。
• 最大性以整除關係刻畫；在自然數中與通常的數值最大公因數一致。

符號作用域

• d — 最大公因數
• g — 最大公因數運算
• a — 第一自然數
• b — 第二自然數

直觀、定義與常見誤解

歐幾里得算法反覆以非零除數的餘數取代較大輸入，直到餘數為零；最後非零值是 gcd。對 (0,0) 另採 0。

驗證候選 d 不只要檢查 d 同時整除兩數，還要檢查全部公因數都整除 d；只找到一個大公因數不夠。

互質不表示兩數都是質數。例如 8 與 15 互質；0 與 1 互質，但 0 與大於 1 的數不互質。

把任何共同因數稱為最大公因數，或把互質誤解成兩個數本身都必須是質數。

已採用的推導導讀

原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。

前置知識

• 自然數整除 — 公因數與最大性都以整除關係表達。

驗證界線

自然數上的歐幾里得算法可精確重算；本輪不建立 Bézout 整數係數的形式證明。

not_formalized

這不表示內容錯誤；只表示尚未登錄可重播的計算或形式證據。

下一個義務

綁定 Nat.gcd、Nat.dvd_gcd、Nat.gcd_dvd_left/right、gcd_greatest 與 Nat.Coprime。

同源結構化資料

本頁與互動版共用同一個物件與既有語言 edition；未新增證明或人工審定。