# 有限整環：以完整乘法表判定 ℤ/5ℤ 與 ℤ/6ℤ，再由有限性推出可逆

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-finite-integral-domain/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-finite-integral-domain-01 · production-20261019-adopted-96



## 目標與範圍

以完整乘法表判定 ℤ/5ℤ 是有限整環、ℤ/6ℤ 不是；再把「每個非零元可逆」作為定義之後的定理，對任何有限整環用有限性證明，並在 ℤ/5ℤ 中求出全部逆元，同時說明 ℤ/6ℤ 中 2 為何沒有逆元。

只在 MKO 範圍內工作：父結構已是完整有限交換含一環（ℤ/5ℤ 與 ℤ/6ℤ，加法與乘法表取模給出，假設 a1）；無零因子的條件對全部非零元素對量化（假設 a2）。可逆性定理對一般有限整環證明。不證明「ℤ/nℤ 是整環當且僅當 n 為質數」的一般判準，不建立有限域節點；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- divides_def
- division_algorithm
- distributive
- finite_counting_basics
- quantifier_negation
- injective_surjective_def
- case_analysis


- G1 — R5=ℤ/5ℤ={0,1,2,3,4}，加法與乘法是整數運算後取除以 5 的餘數；完整的加法表與乘法表由此確定，R5 已是有限交換含一環（MKO 假設 a1）。
- G2 — R6=ℤ/6ℤ={0,1,2,3,4,5}，運算同上但取模 6；R6 也已是有限交換含一環。
- G3 — 定義 D(R)：有限交換含一環 R 是有限整環，若 1≠0，且對所有 a,b∈R，a≠0、b≠0 ⇒ ab≠0（量化全部非零元素對，MKO 假設 a2）。定義中沒有「非零元可逆」。


- \mathbb{Z}/n\mathbb{Z} — 模 n 的剩餘類環，元素記為 0 到 n−1
- D(R) — R 是有限整環
- \lambda_a — 乘以 a 的映射 x↦ax
- a^{-1} — a 的乘法逆元
- R\setminus\{0\} — R 的非零元素





## 規則與來源


- divides_def · prerequisite — 整除：對整數 a、b，a∣b 表示存在整數 k 使 b=ak。
- division_algorithm · prerequisite — 帶餘除法：對整數 a 與正整數 b，存在唯一的整數 q、r 使 a=bq+r 且 0≤r<b。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- injective_surjective_def · prerequisite — 單射：f(a)=f(a′) ⇒ a=a′。滿射：每個 b∈B 都有 a∈A 使 f(a)=b。雙射：既單又滿，此時有唯一反函數 f⁻¹ 使 f⁻¹∘f=id_A、f∘f⁻¹=id_B。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- mul_one · prerequisite — 乘法單位元：1·u=u。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
- image_preimage_def · prerequisite — 像與原像：f(S)={f(a) ∣ a∈S}；f⁻¹(T)={a∈A ∣ f(a)∈T}。原像記號不預設 f 有反函數。
- subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
- set_operations_def · prerequisite — 集合運算：x∈A∪B ⇔ x∈A 或 x∈B；x∈A∩B ⇔ x∈A 且 x∈B；x∈A∖B ⇔ x∈A 且 x∉B；在全集 U 中 Aᶜ=U∖A。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- exists_elim · prerequisite — ∃消去：由 ∃x∈D, P(x)，可取一個新名字 a 表示某個滿足 P(a) 的元素；只要最後結論不含 a，就可用 a 推理。
- mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
- zero_product · prerequisite — 零乘積性質：在 ℤ、ℚ、ℝ、ℂ（或任何整域）中，uv=0 ⇔ u=0 或 v=0。
- mko_fid_def · cited — 在同一完整有限交換含一環表上，若對所有非零 a,b 皆有 a 乘 b 不等於 0，則為有限整環。完整表可逐對核零因子；每個非零元可逆是利用有限性的後續定理步驟，不偷放入定義。 · mko-finite-integral-domain
- mod_reduce · prerequisite — 在 ℤ/nℤ 中，整數 m 代表它除以 n 的餘數 r（0≤r<n）；兩個整數代表同一元素當且僅當 n 整除兩者之差；兩元素的積是整數積的餘數。
- ring_axioms · prerequisite — 交換含一環：加法成交換群，乘法結合、交換、有單位元 1，且分配律成立；由此 a·0=0 且 a(x−y)=ax−ay。
- L_lambda_injective · lemma — 在整環 R 中，若 a≠0，則 λ_a(x)=ax 是單射：ax=ay ⇒ x=y。
- L_finite_inj_surj · lemma — 有限集 S 上的單射 f:S→S 必為滿射。





## 逐步主鏈

S01 · definition操作前

D(\mathbb{Z}/5\mathbb{Z})

操作後

\text{(i) ring (G1)}\ \land\ \text{(ii) }1\neq 0\ \land\ \text{(iii) }\forall a,b\in R_5\setminus\{0\}:\ ab\neq 0

條件：無

規則：mko_fid_def · 依賴：G1, G3

葉節點依據：def_unfold + mko_fid_def

展開定義：要核三件事。(i) 父結構已是完整有限交換含一環（G1，MKO 假設 a1）；(ii) 1≠0；(iii) 每一對非零元素的積非零。定義中沒有「每個非零元可逆」，那是 S08 到 S10 才證明的定理。



S02 · implies操作前

1,0\in\mathbb{Z}/5\mathbb{Z}

操作後

1\neq 0

條件：無

規則：mod_reduce · 依賴：G1, mod_reduce

葉節點依據：mod_reduce + divides_def + division_algorithm

兩個整數在 ℤ/5ℤ 中代表同一元素當且僅當 5 整除其差。1−0=1，而 5 不整除 1（0<1<5，1 不是 5 的倍數）。所以 1≠0，條件 (ii) 成立；這是父含一環保留下來的條件（MKO 段落 0）。



S03 · equivalent操作前

\forall (a,b)\in\{1,2,3,4\}^2:\ ab\neq 0

操作後

\forall a\le b\ \text{in}\ \{1,2,3,4\}:\ ab\neq 0

條件：無

規則：mul_comm · 依賴：G1, S01

葉節點依據：mul_comm + forall_elim + finite_counting_basics

非零元素是 1、2、3、4，有序對共 16 個。⇒：右邊只是左邊的特例。⇐：對任一有序對 (a,b)，若 a≤b 已在右邊清單；若 a>b，則 ab=ba 且 (b,a) 滿足 b<a，也在清單中。所以只需算 4 個平方加 C(4,2)=6 個相異元素的乘積，共 10 個（N4）。



S04 · equivalent操作前

ab\ (1\le a\le b\le 4)\ \text{in}\ \mathbb{Z}/5\mathbb{Z}

操作後

1\cdot b=b;\ 2\cdot2=4,\ 2\cdot3=1,\ 2\cdot4=3,\ 3\cdot3=4,\ 3\cdot4=2,\ 4\cdot4=1

條件：無

規則：mod_reduce · 依賴：S03, G1

葉節點依據：mod_reduce + numeric_evaluation

逐一算出 S03 的 10 個乘積：含 1 的 4 個在 S04.1，其餘 6 個在 S04.2。這是乘法表中所需部分的完整列出。



S05 · implies操作前

\text{the 10 products lie in }\{1,2,3,4\}

操作後

\forall a,b\in R_5\setminus\{0\}:\ ab\neq 0

條件：無

規則：case_analysis · 依賴：S03, S04, S04.1, S04.2

葉節點依據：case_analysis + forall_intro

10 個乘積都在 {1,2,3,4} 中，沒有一個是 0。由 S03，這 10 種情況涵蓋全部 16 個非零有序對，所以全稱的條件 (iii) 成立。這是對整個有限集合的窮舉，每一對都被核到，不是抽樣；N3 另把 16 個有序對逐一重算，它恰好涵蓋此有限集合的全部情況。



S06 · implies操作前

\text{(i)},\ \text{(ii)},\ \text{(iii) for }R_5

操作後

D(\mathbb{Z}/5\mathbb{Z})

條件：無

規則：and_intro_elim · 依賴：S01, S02, S05, G1

葉節點依據：and_intro_elim + def_unfold

(i) 由 G1，(ii) 由 S02，(iii) 由 S05。三者合取，依 S01 的展開，ℤ/5ℤ 是有限整環。



S07 · implies操作前

2,3\in R_6\setminus\{0\}

操作後

2\cdot 3=0\ \text{in}\ \mathbb{Z}/6\mathbb{Z},\ \text{hence}\ \neg D(\mathbb{Z}/6\mathbb{Z})

條件：無

規則：quantifier_negation · 依賴：G2, G3, mod_reduce

葉節點依據：quantifier_negation + mod_reduce + numeric_evaluation

在 ℤ/6ℤ 中 2≠0、3≠0（6 不整除 2 或 3），但 2·3=6=1·6+0，所以 2·3=0（N5）。這一對使 (iii) 的否定「存在非零 a、b 使 ab=0」成立；依量詞否定，全稱的 (iii) 不成立，所以 ℤ/6ℤ 不是有限整環，雖然它的 1≠0 仍成立。另有 3·4=12≡0（N6）。否定一個全稱命題，一個反例就夠。



S08 · implies操作前

D(R),\ a\in R\setminus\{0\},\ \lambda_a(x)=ax

操作後

\lambda_a:R\to R\ \text{injective}

條件：a\neq 0

規則：L_lambda_injective · 依賴：G3

葉節點依據：distributive + contrapositive + injective_surjective_def

以下對任何有限整環 R 與任何 a≠0 工作，不再只看 ℤ/5ℤ。定義 λ_a:R→R，x↦ax。依引理 L_lambda_injective（在 S08.1、S08.2 證明），λ_a 是單射。這一步只用到無零因子，尚未用到有限性。



S09 · implies操作前

\lambda_a:R\to R\ \text{injective},\ R\ \text{finite}

操作後

\lambda_a(R)=R

條件：R\ \text{finite}

規則：L_finite_inj_surj · 依賴：S08

葉節點依據：finite_counting_basics + injective_surjective_def

依引理 L_finite_inj_surj（在 S09.1、S09.2 證明），有限集上的單射自映射是滿射，所以 λ_a 的像是整個 R。這是整個論證中第一次、也是唯一一次用到 R 有限。



S10 · implies操作前

1\in R=\lambda_a(R)

操作後

\exists b\in R:\ ab=ba=1

條件：無

規則：image_preimage_def · 依賴：S09, ring_axioms

葉節點依據：image_preimage_def + exists_elim + mul_comm + mul_assoc

1∈R=λ_a(R)，依像的定義存在 b∈R 使 λ_a(b)=ab=1；由交換律 ba=1。所以 a 可逆。逆元唯一：若 ab=ac=1，則 b=b(ac)=(ba)c=c。這是定義之後、用到有限性的定理（MKO 段落 2）。



S11 · implies操作前

\lambda_2\ \text{on}\ \mathbb{Z}/5\mathbb{Z}

操作後

(0,1,2,3,4)\mapsto(0,2,4,1,3);\ 2^{-1}=3,\ 3^{-1}=2,\ 4^{-1}=4,\ 1^{-1}=1

條件：無

規則：mod_reduce · 依賴：S06, S10, S04.2

葉節點依據：mod_reduce + numeric_evaluation

λ_2 的值：2·0=0、2·1=2、2·2=4、2·3=6≡1、2·4=8≡3（N7）。五個值互異，是 R5 的一個排列，正如 S08、S09 所預測。1=λ_2(3)，所以 2^{-1}=3。由 S04.2：3·2=1、4·4=1；又 1·1=1。故 R5 的每個非零元都可逆，這裡逐一算出，與 S10 一致。



S12 · implies操作前

\lambda_2\ \text{on}\ \mathbb{Z}/6\mathbb{Z}

操作後

(0,1,2,3,4,5)\mapsto(0,2,4,0,2,4);\ 1\notin\lambda_2(R_6)

條件：無

規則：mod_reduce · 依賴：S07, G2

葉節點依據：mod_reduce + numeric_evaluation + injective_surjective_def

在 ℤ/6ℤ 中 2·3=6≡0=2·0、2·4=8≡2=2·1、2·5=10≡4=2·2（N8）。λ_2 不是單射，像只有 {0,2,4}，不含 1，所以 2 在 ℤ/6ℤ 中沒有逆元。S08 的論證在 S08.2 斷掉：2(3−0)=0 而 3−0≠0，正是 S07 的零因子。



S13 · implies操作前

2b=1,\ b\in\mathbb{Z}

操作後

\text{no solution: }2\ \text{is not invertible in}\ \mathbb{Z}

條件：無

規則：divides_def · 依賴：divides_def

葉節點依據：divides_def + division_algorithm + zero_product

ℤ 是無零因子的交換含一環（零乘積性質），但不是有限的。若 2b=1 有整數解，則 2∣1；但 1 不是 2 的倍數（0<1<2）。所以 2 在 ℤ 中不可逆。這說明 S09 的有限性不可省略：無零因子本身推不出可逆，所以可逆性不能偷放入定義。



S14 · implies操作前

D(\mathbb{Z}/5\mathbb{Z}),\ \neg D(\mathbb{Z}/6\mathbb{Z}),\ \text{S08 to S10}

操作後

\mathbb{Z}/5\mathbb{Z}\ \text{finite integral domain};\ \mathbb{Z}/6\mathbb{Z}\ \text{not};\ D(R)\Rightarrow\text{every }a\neq0\ \text{invertible}

條件：無

規則：and_intro_elim · 依賴：S06, S07, S10, S11, S12

葉節點依據：and_intro_elim

完整表的窮舉核對給出 D(ℤ/5ℤ)；一個零因子對給出 ¬D(ℤ/6ℤ)；對任何有限整環，S08 到 S10 證明每個非零元可逆，S11 在 ℤ/5ℤ 中逐一算出逆元。







## 局部子步與引理

S04.1 · equivalent操作前

1\cdot b,\ b\in\{1,2,3,4\}

操作後

1\cdot b=b\neq 0

條件：無

規則：mul_one · 依賴：G1, mul_one

葉節點依據：mul_one

1 是乘法單位元，1·b=b；b 非零，所以 1·1、1·2、1·3、1·4 都非零。



S04.2 · equivalent操作前

2\cdot2,\ 2\cdot3,\ 2\cdot4,\ 3\cdot3,\ 3\cdot4,\ 4\cdot4

操作後

4,\ 1,\ 3,\ 4,\ 2,\ 1

條件：無

規則：mod_reduce · 依賴：G1, mod_reduce

葉節點依據：mod_reduce + division_algorithm + numeric_evaluation

先在 ℤ 中相乘得 4、6、8、9、12、16，再取除以 5 的餘數：4=0·5+4、6=1·5+1、8=1·5+3、9=1·5+4、12=2·5+2、16=3·5+1。所以六個積依序為 4、1、3、4、2、1（N1、N2）。



S08.1 · equivalent操作前

ax=ay

操作後

a(x-y)=0

條件：無

規則：distributive · 依賴：ring_axioms

葉節點依據：distributive + eq_congruence + add_inverse + neg_mul

兩邊同減 ay 得 ax−ay=0；由分配律 ax−ay=ax+a(−y)=a(x−y)。反向：由 a(x−y)=0 得 ax−ay=0，兩邊同加 ay 得 ax=ay。



S08.2 · implies操作前

a(x-y)=0,\ a\neq 0

操作後

x=y

條件：a\neq 0

規則：contrapositive · 依賴：S08.1, G3

葉節點依據：contrapositive + add_inverse + eq_congruence

若 x−y≠0，則 a 與 x−y 都非零，依定義 (iii) a(x−y)≠0，與 S08.1 矛盾。所以 x−y=0，兩邊同加 y 得 x=y。S08.1 與 S08.2 合起來證得引理 L_lambda_injective。



S09.1 · implies操作前

\lambda_a\ \text{injective}

操作後

|\lambda_a(R)|=|R|

條件：無

規則：finite_counting_basics · 依賴：S08, finite_counting_basics, injective_surjective_def

葉節點依據：finite_counting_basics + injective_surjective_def + image_preimage_def

把 λ_a 看成 R→λ_a(R) 的函數：依像的定義它是滿射，又是單射，所以是雙射。有限集之間有雙射當且僅當元素個數相同，故 |λ_a(R)|=|R|。論證對任何有限集上的單射自映射都相同。



S09.2 · implies操作前

\lambda_a(R)\subseteq R,\ |\lambda_a(R)|=|R|

操作後

\lambda_a(R)=R

條件：R\ \text{finite}

規則：finite_counting_basics · 依賴：S09.1, subset_def

葉節點依據：finite_counting_basics + set_operations_def + contradiction

若 λ_a(R)≠R，則 R∖λ_a(R) 非空，R 是不交有限集 λ_a(R) 與 R∖λ_a(R) 的聯集，|R|=|λ_a(R)|+|R∖λ_a(R)|≥|λ_a(R)|+1，與 S09.1 矛盾。所以 λ_a(R)=R。S09.1 與 S09.2 合起來證得引理 L_finite_inj_surj。







## 逐步反向審查


- S14 · sufficient_goal_reduction · S06, S07, S10, S11 — 目標 G：判定兩個環並證明可逆性定理。足夠條件 H：S06、S07、S10、S11；H⇒G 由合取。H 由 G1 到 G3 正向證成，沒有把 G 當作前提，也沒有把可逆性當作定義的一部分。
- S13 · premise_audit · divides_def, zero_product — ℤ 不屬於 D 的論域（D 只談有限環），這裡只作為對照，說明有限性的作用。
- S12 · premise_audit · S07, mod_reduce — 六個值逐一可重算；1 不在像中這一點對 6 個輸入是完整核對。
- S11 · premise_audit · S06, S10, S04.2, mod_reduce — 每個逆元都可直接乘回核對；這些計算是 S10 在一個例子上的實例，不取代 S10 的一般證明。
- S10 · premise_audit · S09, image_preimage_def, ring_axioms — 需要 S09 的滿射；不宣稱反向，即可逆性不能反過來當作 D(R) 的定義條款。
- S09.2 · premise_audit · S09.1, finite_counting_basics, contradiction — 加法公式 |A∪B|=|A|+|B| 只對有限集給出矛盾；無限集的真子集可以與全集等大。
- S09.1 · premise_audit · S08, finite_counting_basics, image_preimage_def — 需要單射；非單射的映射（如 ℤ/6ℤ 的 λ_2）其像較小。
- S09 · premise_audit · S08, L_finite_inj_surj — 需要單射與有限兩個前提；對無限集不成立：ℤ 中 x↦2x 是單射但不是滿射。
- S08.2 · premise_audit · S08.1, G3, contrapositive — 這裡用的是 (iii) 的逆否形式；沒有 (iii) 時，ℤ/6ℤ 的 2(3−0)=0 而 3−0≠0 正是反例。
- S08.1 · inverse_equivalence · distributive, eq_congruence, add_inverse — 加減 ay 互為反運算，分配律是恆等式，所以雙向成立。
- S08 · premise_audit · G3, L_lambda_injective — 需要 a≠0 與定義的 (iii)；在 ℤ/6ℤ 中 a=2 時結論失敗（S12）。
- S07 · premise_audit · G2, mod_reduce, quantifier_negation — 只需一個零因子對；本步不宣稱找出了全部零因子。
- S06 · premise_audit · S01, S02, S05, G1 — 三項都需要；此步沒有用到可逆性。
- S05 · premise_audit · S03, S04, case_analysis — 需要情況完整（S03 的化約與 S04 的完整列表）；只核其中幾個乘積不能推出全稱命題。
- S04.2 · inverse_equivalence · mod_reduce, division_algorithm — 反向核對：4−4、6−1、8−3、9−4、12−2、16−1 依序為 0、5、5、5、10、15，都是 5 的倍數；餘數由帶餘除法唯一決定。
- S04.1 · inverse_equivalence · mul_one — 1·b=b 是恆等式，兩邊互換即反向。
- S04 · inverse_equivalence · mod_reduce, numeric_evaluation — 每個結果都可反向核對：整數積減去所寫的餘數是 5 的倍數；兩邊表示同一元素。
- S03 · inverse_equivalence · mul_comm, forall_elim — 兩個方向都有理由：特例化給 ⇒，交換律給 ⇐。化約只減少計算量，不減少被覆蓋的情況。
- S02 · premise_audit · mod_reduce, divides_def — 只需要 5∤1。在 ℤ/1ℤ 中 1−0=1 是 1 的倍數，1=0，條件 (ii) 會失敗。
- S01 · premise_audit · G1, G3, mko_fid_def — 此步只展開定義，不推出新事實；三項之一不成立，D(R5) 就不成立。





## 錯誤控制與反例

抽查乘積不是證書MKO 指出的誤解：抽查後宣稱無零因子。在 ℤ/6ℤ 中 1·5=5、5·5=25≡1、2·2=4、3·3=9≡3、4·4=16≡4、2·5=10≡4 都非零，但 2·3≡0、3·4≡0。本稿選用對全部非零元素對完整窮舉的證書（ℤ/6ℤ 有 5+C(5,2)=15 個無序對，N9），ℤ/5ℤ 的 S03 到 S05 就採此法；但它不是唯一可能的證法。例如可先直接核出每個非零元的逆元，再把 ab=0 乘以 a 的逆元推出 b=0。這個替代證書的逆元必須獨立核得，不能循環引用本稿稍後先假設整環才證得的可逆性定理。

可逆不放入定義MKO 的第二個誤解是把「非零元可逆」直接塞進定義。本稿把它放在 S08 到 S10 作為定理，並指出唯一用到有限性的是 S09。ℤ 無零因子但 2 不可逆（S13），所以沒有有限性這個定理就不成立。

在 ℤ/nℤ 中計算，而不是在 ℤ 中2·3=6 在 ℤ 中非零，但在 ℤ/6ℤ 中 6 的餘數是 0。每個乘積都要取模後再判斷是否為 0（S04.2、S07）。


- 在 ℤ/6ℤ 中抽查 1·5、5·5、2·2、3·3 都非零，所以 ℤ/6ℤ 是整環 → reject — 2·3=6≡0，2、3 都非零；抽樣不能證明全稱命題。
- 依定義，整環的每個非零元都可逆 → reject — 定義只要求無零因子；ℤ 中 2 不可逆。有限整環的可逆性是用有限性證出的定理。
- 乘法表中 0 的那一行全是 0，所以每個環都有零因子 → reject — 零因子要求兩個因子都非零；a·0=0 不算。ℤ/5ℤ 沒有零因子（S05）。
- 零環 {0} 沒有非零元素對，所以是有限整環 → reject — 定義要求 1≠0；零環中 1=0。





## 結論與限制

ℤ/5ℤ 是有限整環：1≠0，且完整窮舉 16 個非零有序對（化為 10 個乘積）沒有一個積為 0。ℤ/6ℤ 不是：2·3=0。對任何有限整環，乘以非零 a 的映射是單射，有限性使它成為滿射，所以 a 可逆；在 ℤ/5ℤ 中 2^{-1}=3、3^{-1}=2、4^{-1}=4、1^{-1}=1。可逆性是定義之後的定理，ℤ 顯示沒有有限性時它可以失敗。


- 本稿不證明一般判準「ℤ/nℤ 是整環當且僅當 n 為質數」，只對 n=5、6 用完整表判定。有限域節點（MKO 的下一步）另立；本稿只指出 S10 使 ℤ/5ℤ 的非零元可逆。





## 驗證及來源綁定

9 個本稿宣告算術檢查；只支持所列算式。


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 6842601da20f360629d3dee64daf3c9fc262cafcaa31e16bfde9af109e74d478
- original source SHA-256: c6d77ede514c66536e880f8031f33ef853dd3bf2f798b17a549fcac1447b8f09
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-finite-integral-domain-01.json)