# Finite integral domain: deciding ℤ/5ℤ and ℤ/6ℤ from complete tables, then deriving invertibility from finiteness

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-finite-integral-domain/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

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



## Goal and scope

Using complete multiplication tables, decide that ℤ/5ℤ is a finite integral domain and ℤ/6ℤ is not; then prove, as a theorem that comes after the definition, that every nonzero element of any finite integral domain is invertible, using finiteness; find all inverses in ℤ/5ℤ and explain why 2 has no inverse in ℤ/6ℤ.

Works inside the MKO's scope: the parent structure already is a complete finite commutative unital ring (ℤ/5ℤ and ℤ/6ℤ, with tables given by reduction modulo n, assumption a1), and the no-zero-divisor condition is quantified over every pair of nonzero elements (assumption a2). The invertibility theorem is proved for a general finite integral domain. It does not prove the general criterion that ℤ/nℤ is a domain exactly when n is prime, and does not set up the finite-field node; it does not change the canonical MKO or its English edition.





## Givens and symbols


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


- G1 — R5=ℤ/5ℤ={0,1,2,3,4}, with addition and multiplication given by the integer operation followed by the remainder on division by 5; this fixes the complete addition and multiplication tables, and R5 already is a finite commutative unital ring (MKO assumption a1).
- G2 — R6=ℤ/6ℤ={0,1,2,3,4,5}, with the same operations taken modulo 6; R6 also is a finite commutative unital ring.
- G3 — Definition D(R): a finite commutative unital ring R is a finite integral domain if 1≠0 and, for all a,b∈R, a≠0 and b≠0 ⇒ ab≠0 (quantified over every pair of nonzero elements, MKO assumption a2). The definition contains no clause about nonzero elements being invertible.


- \mathbb{Z}/n\mathbb{Z} — integers modulo n, elements written 0 to n−1
- D(R) — R is a finite integral domain
- \lambda_a — the multiplication map x↦ax
- a^{-1} — the multiplicative inverse of a
- R\setminus\{0\} — the nonzero elements of R





## Rules and sources


- divides_def · prerequisite — Divisibility: for integers a, b, a∣b means there is an integer k with b=ak.
- division_algorithm · prerequisite — Division algorithm: for an integer a and a positive integer b there are unique integers q, r with a=bq+r and 0≤r<b.
- distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
- finite_counting_basics · prerequisite — Finite counting: for disjoint finite sets A, B, |A∪B|=|A|+|B|; |A×B|=|A|·|B|; there is a bijection between finite sets ⇔ they have the same number of elements.
- quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
- injective_surjective_def · prerequisite — Injective: f(a)=f(a′) ⇒ a=a′. Surjective: every b∈B has some a∈A with f(a)=b. Bijective: both; then there is a unique inverse f⁻¹ with f⁻¹∘f=id_A and f∘f⁻¹=id_B.
- case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
- def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
- mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
- forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- mul_one · prerequisite — Multiplicative identity: 1·u=u.
- forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
- eq_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule.
- add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
- neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
- image_preimage_def · prerequisite — Image and preimage: f(S)={f(a) ∣ a∈S}; f⁻¹(T)={a∈A ∣ f(a)∈T}. The preimage notation does not presuppose that f has an inverse.
- subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
- set_operations_def · prerequisite — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A.
- contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
- exists_elim · prerequisite — ∃-elimination: from ∃x∈D, P(x) we may name some element a with P(a) by a fresh name; reasoning with a is allowed as long as the final conclusion does not mention a.
- mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
- zero_product · prerequisite — Zero-product property: in ℤ, ℚ, ℝ, ℂ (or any integral domain), uv=0 ⇔ u=0 or v=0.
- mko_fid_def · cited — Using the same complete finite commutative unital-ring tables, require a*b to differ from zero for every pair of nonzero elements. The complete table supports an exhaustive zero-divisor audit. Invertibility of every nonzero element is a subsequent theorem using finiteness, not silently inserted into this definition. · mko-finite-integral-domain
- mod_reduce · prerequisite — In ℤ/nℤ an integer m stands for its remainder r on division by n (0≤r<n); two integers stand for the same element exactly when n divides their difference; the product of two elements is the remainder of the integer product.
- ring_axioms · prerequisite — Commutative unital ring: addition forms a commutative group, multiplication is associative and commutative with identity 1, and distributivity holds; hence a·0=0 and a(x−y)=ax−ay.
- L_lambda_injective · lemma — In an integral domain R, if a≠0 then λ_a(x)=ax is injective: ax=ay ⇒ x=y.
- L_finite_inj_surj · lemma — An injective map f:S→S on a finite set S is surjective.





## Main derivation

S01 · definitionBefore

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

After

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

Conditions: none

Rule: mko_fid_def · Uses: G1, G3

Leaf basis: def_unfold + mko_fid_def

Unfold the definition: three things must be checked. (i) The parent structure already is a complete finite commutative unital ring (G1, MKO assumption a1); (ii) 1≠0; (iii) the product of every pair of nonzero elements is nonzero. The definition has no clause 'every nonzero element is invertible'; that is a theorem proved only in S08 to S10.



S02 · impliesBefore

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

After

1\neq 0

Conditions: none

Rule: mod_reduce · Uses: G1, mod_reduce

Leaf basis: mod_reduce + divides_def + division_algorithm

Two integers stand for the same element of ℤ/5ℤ exactly when 5 divides their difference. 1−0=1, and 5 does not divide 1 (0<1<5, so 1 is not a multiple of 5). Hence 1≠0 and condition (ii) holds; it is inherited from the parent unital ring (MKO paragraph 0).



S03 · equivalentBefore

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

After

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

Conditions: none

Rule: mul_comm · Uses: G1, S01

Leaf basis: mul_comm + forall_elim + finite_counting_basics

The nonzero elements are 1, 2, 3, 4, giving 16 ordered pairs. ⇒: the right side is a special case of the left. ⇐: for any ordered pair (a,b), if a≤b it is on the right-hand list; if a>b, then ab=ba and (b,a) has b<a, so it is on the list too. Hence only 4 squares plus C(4,2)=6 products of distinct elements, 10 products in all, need computing (N4).



S04 · equivalentBefore

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

After

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

Conditions: none

Rule: mod_reduce · Uses: S03, G1

Leaf basis: mod_reduce + numeric_evaluation

Compute the 10 products of S03 one by one: the 4 involving 1 in S04.1 and the other 6 in S04.2. This lists the required part of the multiplication table completely.



S05 · impliesBefore

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

After

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

Conditions: none

Rule: case_analysis · Uses: S03, S04, S04.1, S04.2

Leaf basis: case_analysis + forall_intro

All 10 products lie in {1,2,3,4}; none is 0. By S03 these 10 cases cover all 16 nonzero ordered pairs, so the universal condition (iii) holds. This is an exhaustion of the whole finite set in which every pair is checked, not a sample; N3 recomputes the 16 ordered pairs one by one, and it covers exactly all cases of this finite set.



S06 · impliesBefore

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

After

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

Conditions: none

Rule: and_intro_elim · Uses: S01, S02, S05, G1

Leaf basis: and_intro_elim + def_unfold

(i) comes from G1, (ii) from S02 and (iii) from S05. Their conjunction gives, by the unfolding in S01, that ℤ/5ℤ is a finite integral domain.



S07 · impliesBefore

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

After

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

Conditions: none

Rule: quantifier_negation · Uses: G2, G3, mod_reduce

Leaf basis: quantifier_negation + mod_reduce + numeric_evaluation

In ℤ/6ℤ we have 2≠0 and 3≠0 (6 divides neither 2 nor 3), but 2·3=6=1·6+0, so 2·3=0 (N5). This pair makes the negation of (iii), 'some nonzero a, b have ab=0', true; by quantifier negation the universal (iii) fails, so ℤ/6ℤ is not a finite integral domain, even though 1≠0 still holds there. Also 3·4=12≡0 (N6). One counterexample suffices to refute a universal statement.



S08 · impliesBefore

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

After

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

Conditions: a\neq 0

Rule: L_lambda_injective · Uses: G3

Leaf basis: distributive + contrapositive + injective_surjective_def

From here on work with any finite integral domain R and any a≠0, not just ℤ/5ℤ. Define λ_a:R→R by x↦ax. By Lemma L_lambda_injective (proved in S08.1 and S08.2), λ_a is injective. This step uses only the absence of zero divisors, not yet finiteness.



S09 · impliesBefore

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

After

\lambda_a(R)=R

Conditions: R\ \text{finite}

Rule: L_finite_inj_surj · Uses: S08

Leaf basis: finite_counting_basics + injective_surjective_def

By Lemma L_finite_inj_surj (proved in S09.1 and S09.2), an injective self-map of a finite set is surjective, so the image of λ_a is all of R. This is the first and only place where the finiteness of R is used.



S10 · impliesBefore

1\in R=\lambda_a(R)

After

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

Conditions: none

Rule: image_preimage_def · Uses: S09, ring_axioms

Leaf basis: image_preimage_def + exists_elim + mul_comm + mul_assoc

1∈R=λ_a(R), so by the definition of image there is b∈R with λ_a(b)=ab=1, and commutativity gives ba=1. Hence a is invertible. The inverse is unique: if ab=ac=1 then b=b(ac)=(ba)c=c. This is a theorem after the definition, and it uses finiteness (MKO paragraph 2).



S11 · impliesBefore

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

After

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

Conditions: none

Rule: mod_reduce · Uses: S06, S10, S04.2

Leaf basis: mod_reduce + numeric_evaluation

Values of λ_2: 2·0=0, 2·1=2, 2·2=4, 2·3=6≡1, 2·4=8≡3 (N7). The five values are distinct, a permutation of R5, as S08 and S09 predict. 1=λ_2(3), so 2^{-1}=3. From S04.2: 3·2=1 and 4·4=1; also 1·1=1. So every nonzero element of R5 is invertible, computed here one by one, in agreement with S10.



S12 · impliesBefore

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

After

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

Conditions: none

Rule: mod_reduce · Uses: S07, G2

Leaf basis: mod_reduce + numeric_evaluation + injective_surjective_def

In ℤ/6ℤ, 2·3=6≡0=2·0, 2·4=8≡2=2·1 and 2·5=10≡4=2·2 (N8). λ_2 is not injective, and its image is only {0,2,4}, which does not contain 1, so 2 has no inverse in ℤ/6ℤ. The argument of S08 breaks at S08.2: 2(3−0)=0 while 3−0≠0, which is exactly the zero divisor of S07.



S13 · impliesBefore

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

After

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

Conditions: none

Rule: divides_def · Uses: divides_def

Leaf basis: divides_def + division_algorithm + zero_product

ℤ is a commutative unital ring without zero divisors (zero-product property), but it is not finite. If 2b=1 had an integer solution, then 2∣1; but 1 is not a multiple of 2 (0<1<2). So 2 is not invertible in ℤ. This shows that the finiteness used in S09 cannot be dropped: the absence of zero divisors alone does not give invertibility, so invertibility must not be slipped into the definition.



S14 · impliesBefore

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

After

\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}

Conditions: none

Rule: and_intro_elim · Uses: S06, S07, S10, S11, S12

Leaf basis: and_intro_elim

Exhaustive checking of the complete table gives D(ℤ/5ℤ); one zero-divisor pair gives ¬D(ℤ/6ℤ); for any finite integral domain S08 to S10 prove that every nonzero element is invertible, and S11 computes the inverses in ℤ/5ℤ one by one.







## Substeps and lemmas

S04.1 · equivalentBefore

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

After

1\cdot b=b\neq 0

Conditions: none

Rule: mul_one · Uses: G1, mul_one

Leaf basis: mul_one

1 is the multiplicative identity, so 1·b=b; b is nonzero, so 1·1, 1·2, 1·3 and 1·4 are all nonzero.



S04.2 · equivalentBefore

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

After

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

Conditions: none

Rule: mod_reduce · Uses: G1, mod_reduce

Leaf basis: mod_reduce + division_algorithm + numeric_evaluation

Multiply in ℤ to get 4, 6, 8, 9, 12, 16, then take remainders on division by 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. So the six products are 4, 1, 3, 4, 2, 1 in order (N1, N2).



S08.1 · equivalentBefore

ax=ay

After

a(x-y)=0

Conditions: none

Rule: distributive · Uses: ring_axioms

Leaf basis: distributive + eq_congruence + add_inverse + neg_mul

Subtract ay from both sides: ax−ay=0; by distributivity ax−ay=ax+a(−y)=a(x−y). Backward: a(x−y)=0 gives ax−ay=0, and adding ay to both sides gives ax=ay.



S08.2 · impliesBefore

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

After

x=y

Conditions: a\neq 0

Rule: contrapositive · Uses: S08.1, G3

Leaf basis: contrapositive + add_inverse + eq_congruence

If x−y≠0, then a and x−y are both nonzero, and clause (iii) gives a(x−y)≠0, contradicting S08.1. So x−y=0, and adding y to both sides gives x=y. S08.1 and S08.2 together prove Lemma L_lambda_injective.



S09.1 · impliesBefore

\lambda_a\ \text{injective}

After

|\lambda_a(R)|=|R|

Conditions: none

Rule: finite_counting_basics · Uses: S08, finite_counting_basics, injective_surjective_def

Leaf basis: finite_counting_basics + injective_surjective_def + image_preimage_def

Regard λ_a as a map R→λ_a(R): by the definition of image it is surjective, and it is injective, so it is a bijection. Finite sets admit a bijection exactly when they have the same number of elements, so |λ_a(R)|=|R|. The argument is the same for any injective self-map of a finite set.



S09.2 · impliesBefore

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

After

\lambda_a(R)=R

Conditions: R\ \text{finite}

Rule: finite_counting_basics · Uses: S09.1, subset_def

Leaf basis: finite_counting_basics + set_operations_def + contradiction

If λ_a(R)≠R, then R∖λ_a(R) is nonempty and R is the union of the disjoint finite sets λ_a(R) and R∖λ_a(R), so |R|=|λ_a(R)|+|R∖λ_a(R)|≥|λ_a(R)|+1, contradicting S09.1. Hence λ_a(R)=R. S09.1 and S09.2 together prove Lemma L_finite_inj_surj.







## Reverse audits


- S14 · sufficient_goal_reduction · S06, S07, S10, S11 — Goal G: decide the two rings and prove the invertibility theorem. Sufficient condition H: S06, S07, S10 and S11; H⇒G by conjunction. H is proved forwards from G1 to G3; G is never used as a premise, and invertibility is never made part of the definition.
- S13 · premise_audit · divides_def, zero_product — ℤ is outside the domain of D (which concerns finite rings); it is used here only as a contrast showing what finiteness does.
- S12 · premise_audit · S07, mod_reduce — The six values can be recomputed one by one; that 1 is not in the image is a complete check over all 6 inputs.
- S11 · premise_audit · S06, S10, S04.2, mod_reduce — Each inverse can be checked by multiplying back; these computations are an instance of S10 in one example and do not replace its general proof.
- S10 · premise_audit · S09, image_preimage_def, ring_axioms — It needs the surjectivity of S09; no converse is claimed, and invertibility is not turned back into a clause of D(R).
- S09.2 · premise_audit · S09.1, finite_counting_basics, contradiction — The count |A∪B|=|A|+|B| gives a contradiction only for finite sets; an infinite set can be as large as a proper subset.
- S09.1 · premise_audit · S08, finite_counting_basics, image_preimage_def — It needs injectivity; a non-injective map (such as λ_2 on ℤ/6ℤ) has a smaller image.
- S09 · premise_audit · S08, L_finite_inj_surj — It needs both injectivity and finiteness; for infinite sets it fails: x↦2x on ℤ is injective but not surjective.
- S08.2 · premise_audit · S08.1, G3, contrapositive — This uses the contrapositive form of (iii); without (iii), 2(3−0)=0 with 3−0≠0 in ℤ/6ℤ is exactly a counterexample.
- S08.1 · inverse_equivalence · distributive, eq_congruence, add_inverse — Adding and subtracting ay undo each other and distributivity is an identity, so the step holds both ways.
- S08 · premise_audit · G3, L_lambda_injective — It needs a≠0 and clause (iii) of the definition; in ℤ/6ℤ with a=2 the conclusion fails (S12).
- S07 · premise_audit · G2, mod_reduce, quantifier_negation — One zero-divisor pair is enough; this step does not claim to list all zero divisors.
- S06 · premise_audit · S01, S02, S05, G1 — All three items are needed; invertibility is not used in this step.
- S05 · premise_audit · S03, S04, case_analysis — It needs the cases to be complete (the reduction of S03 and the full list of S04); checking only some of the products cannot establish the universal statement.
- S04.2 · inverse_equivalence · mod_reduce, division_algorithm — Backward check: 4−4, 6−1, 8−3, 9−4, 12−2, 16−1 are 0, 5, 5, 5, 10, 15, all multiples of 5; the remainder is unique by the division algorithm.
- S04.1 · inverse_equivalence · mul_one — 1·b=b is an identity; reading it right to left is the backward direction.
- S04 · inverse_equivalence · mod_reduce, numeric_evaluation — Each result can be checked backwards: the integer product minus the stated remainder is a multiple of 5, so both sides name the same element.
- S03 · inverse_equivalence · mul_comm, forall_elim — Both directions have reasons: specialization gives ⇒ and commutativity gives ⇐. The reduction lowers the amount of computation, not the set of cases covered.
- S02 · premise_audit · mod_reduce, divides_def — Only 5∤1 is needed. In ℤ/1ℤ, 1−0=1 is a multiple of 1, so 1=0 and condition (ii) would fail.
- S01 · premise_audit · G1, G3, mko_fid_def — This step only unfolds the definition and derives no new fact; if any one of the three fails, D(R5) fails.





## Error controls and negative controls

Sampled products are not a certificateThe misconception identified in the MKO: declaring no zero divisors after spot checks. In ℤ/6ℤ, 1·5=5, 5·5=25≡1, 2·2=4, 3·3=9≡3, 4·4=16≡4 and 2·5=10≡4 are all nonzero, yet 2·3≡0 and 3·4≡0. This guide selects exhaustive checking of all nonzero pairs as its certificate (ℤ/6ℤ has 5+C(5,2)=15 unordered pairs, N9), as in S03 to S05 for ℤ/5ℤ. It is not the only possible proof: independently verify an inverse for every nonzero a, then multiply ab=0 by that inverse to get b=0. Those inverse witnesses must be checked independently, not obtained circularly from the later theorem that first assumes an integral domain.

Invertibility is not part of the definitionThe second misconception identified in the MKO is to put 'nonzero elements are invertible' straight into the definition. Here it is a theorem in S08 to S10, and the only use of finiteness is S09. ℤ has no zero divisors but 2 is not invertible (S13), so without finiteness the theorem fails.

Compute in ℤ/nℤ, not in ℤ2·3=6 is nonzero in ℤ, but in ℤ/6ℤ the remainder of 6 is 0. Every product must be reduced modulo n before deciding whether it is 0 (S04.2, S07).


- In ℤ/6ℤ the spot checks 1·5, 5·5, 2·2 and 3·3 are nonzero, so ℤ/6ℤ is an integral domain → reject — 2·3=6≡0 with 2 and 3 nonzero; sampling cannot prove a universal statement.
- By definition, every nonzero element of an integral domain is invertible → reject — The definition only requires no zero divisors; 2 is not invertible in ℤ. Invertibility in a finite integral domain is a theorem proved using finiteness.
- The row of 0 in the multiplication table is all zeros, so every ring has zero divisors → reject — Zero divisors need both factors nonzero; a·0=0 does not count. ℤ/5ℤ has none (S05).
- The zero ring {0} has no pairs of nonzero elements, so it is a finite integral domain → reject — The definition requires 1≠0; in the zero ring 1=0.





## Result and limitations

ℤ/5ℤ is a finite integral domain: 1≠0, and exhausting all 16 nonzero ordered pairs (reduced to 10 products) gives no zero product. ℤ/6ℤ is not: 2·3=0. In any finite integral domain multiplication by a nonzero a is injective, finiteness makes it surjective, and so a is invertible; in ℤ/5ℤ, 2^{-1}=3, 3^{-1}=2, 4^{-1}=4 and 1^{-1}=1. Invertibility is a theorem after the definition, and ℤ shows it can fail without finiteness.


- This guide does not prove the general criterion 'ℤ/nℤ is a domain exactly when n is prime'; it decides only n=5 and n=6 from complete tables. The finite-field node (the MKO's next step) is separate; this guide only notes that S10 makes the nonzero elements of ℤ/5ℤ invertible.





## Verification and source binding

9 declared checks for this guide; only the listed expressions are covered.


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

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-finite-integral-domain-01.json)