# 自然數整除

自然數 a 整除 b，表示存在自然數乘數 k 使 b=a·k；零的兩側行為必須分開。

mko-natural-divisibility · definition · v0.10.0



## 數學敘述

對自然數 a、b，a∣b 當且僅當存在自然數 k 使 b=a·k。每個 a 都整除 0；0∣b 當且僅當 b=0。





## 代表公式（精確 TeX）

b=m(a,k)





## 成立條件


- 自然數包含 0，乘法為自然數乘法。
- 整除的見證 k 必須是自然數；不得以非整數商作見證。





## 符號作用域


- a — 候選除數
- b — 被整除數
- m — 自然數乘法
- k — 自然數乘法見證





## 直觀、定義與常見誤解

檢查 a∣b 時先處理 a=0：只有 b=0 時成立。a>0 時可用商餘或直接搜尋 k，但餘數為零才提供整除見證。

a∣0 對所有自然數 a 成立，因為 0=a·0；0∣0 也成立，而且見證不唯一。

整除具有自反性與傳遞性；有限題目會保存明示的乘數見證，不把浮點除法或近似相等當成證據。

看到 b/a 是數值就宣稱 a∣b，或把除數為零一律判成沒有整除關係。





## 已採用的推導導讀

[自然數整除：以乘數見證判定、處理 0 的情形並證明遞移性](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-natural-divisibility-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [自然數](https://ocme.evemisslab.com/zh-Hant/mko/mko-natural-number/) — 論域與零邊界來自自然數。
- [四則運算](https://ocme.evemisslab.com/zh-Hant/mko/mko-arithmetic-operations/) — 整除見證以精確乘法等式表示。





## 驗證界線

有限整數乘法與商餘可精確重算；案例核對不構成全部整除定理的形式證明。

not_formalized

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





## 下一個義務

綁定 Nat.Dvd 的存在乘數定義、dvd_zero、zero_dvd 與傳遞性。





## 同源結構化資料

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

[原始 MKO JSON](https://ocme.evemisslab.com/data/mko/natural-divisibility.json) · [純文字 Markdown](https://ocme.evemisslab.com/zh-Hant/mko/mko-natural-divisibility/index.md)