LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-28 (claude-fable-5)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Every commutative division ring is a field, so "field" and "commutative division ring" name the same structures and the published definition and the ring-theoretic one agree

Statement

Let $D$ be a commutative division ring (Division ring: a ring with $1 \neq 0$ in which every nonzero element is a unit, Commutative ring), with addition $+$ , multiplication $\cdot$ , zero $0$ and identity $1$ . Then $D$ , with the same operations and the same two distinguished elements, satisfies the axioms (A), (M) and (D) of Field; that is, $D$ is a field.

Together with Every field is a commutative ring with $1 \neq 0$ ; it is an integral domain, and it is a commutative division ring this says that "field" and "commutative division ring" name exactly the same structures, so the published definition of a field and the ring-theoretic description of one agree and no second notion of field is introduced on this page.

Facts & Assumptions

Given: A commutative division ring $D$ with zero $0$ , identity $1$ , $1 \neq 0$ , and $x^{- 1}$ the two-sided multiplicative inverse of each $x \neq 0$ (Division ring: a ring with $1 \neq 0$ in which every nonzero element is a unit, Commutative ring).

[L1]

$(D, +, 0)$ is an abelian group, $(D, \cdot, 1)$ is a monoid, both distributive laws hold, and multiplication is commutative (Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides, Commutative ring, Group and abelian group).

[L2]

$1 \neq 0$ , and every $x \neq 0$ has a two-sided inverse $x^{- 1}$ ; equivalently $D^{\times} = D ∖ {0}$ (Division ring: a ring with $1 \neq 0$ in which every nonzero element is a unit).

[L3]

$D^{\times}$ contains $1$ , is closed under multiplication and under inversion, and is a group under the restricted multiplication; and $0 \in D^{\times}$ only when $1 = 0$ (The units of a ring are the invertible elements of its multiplicative monoid, and $R^{\times}$ is a group under multiplication; $0 \in R^{\times}$ only in the zero ring, Left inverse, right inverse, and invertible element of a monoid, Group and abelian group).

[L4]

$x \cdot 0 = 0 = 0 \cdot x$ for every $x \in D$ (In any ring $0 \cdot a = a \cdot 0 = 0$ , $(- a) b = a (- b) = - (a b)$ , $(- a) (- b) = a b$ , $(- 1) a = - a$ and $a (b - c) = a b - a c$ ).

[L5]

The field axioms to be verified: (A) $(F, +)$ is an abelian group with identity $0$ ; (M) multiplication is associative and commutative on all of $F$ with $x \cdot 1 = x$ for every $x \in F$ , and $(F ∖ {0}, \cdot)$ is an abelian group with identity $1$ , each $x \neq 0$ having an inverse; (D) $x (y + z) = x y + x z$ ; and $0 \neq 1$ (Field).

Proof

technique · direct

1.1

Axiom (A) holds: $(D, +, 0)$ is an abelian group by [L1], which is precisely what (A) asserts.

L1L5

1.2

Axiom (D) holds: the left distributive law $x (y + z) = x y + x z$ is one of the two distributive laws of a ring.

L1L5

1.3

$0 \neq 1$ holds, by [L2].

L2L5

1.4

$D^{\times} = D ∖ {0}$ : every nonzero element is a unit by [L2]; and $0$ is not a unit, since $0 \cdot v = 0$ for every $v$ by [L4], so $0 \cdot v = 1$ would force $1 = 0$ , contradicting [L2].

L2L3L4

2.1

$D ∖ {0}$ is a group under the restricted multiplication, with identity $1$ : this is [L3] applied to $D^{\times}$ , which by step 1.4 is $D ∖ {0}$ . In particular $D ∖ {0}$ is closed under multiplication, so $D$ has no zero divisors.

step 1.4L3

2.2

That group is abelian, since multiplication is commutative on all of $D$ and therefore on the subset $D ∖ {0}$ .

step 1.4L1

3.1

Axiom (M) holds in both of its clauses: multiplication is associative and commutative on all of $D$ with $x \cdot 1 = x$ for every $x \in D$ , since $(D, \cdot, 1)$ is a commutative monoid by [L1]; and $(D ∖ {0}, \cdot)$ is an abelian group with identity $1$ by steps 2.1 and 2.2.

step 2.1step 2.2L1L5

4.1

By steps 1.1, 1.2, 1.3 and 3.1 the structure $(D, +, \cdot, 0, 1)$ satisfies (A), (M), (D) and $0 \neq 1$ , so it is a field.

step 1.1step 1.2step 1.3step 3.1L5∎

Remarks

Both directions are needed, and each is a numbered item. This lemma turns a commutative division ring into a field; Every field is a commutative ring with $1 \neq 0$ ; it is an integral domain, and it is a commutative division ring turns a field into a commutative division ring. Without the pair, the page would carry two unrelated words for one class of structures, which is exactly the defect the page exists to avoid.
Both clauses of axiom (M) are verified separately. (M) asserts associativity, commutativity and $x \cdot 1 = x$ on all of $F$ , and that $(F ∖ {0}, \cdot)$ is an abelian group. A commutative division ring supplies the first clause directly from its ring axioms, its multiplication being a commutative monoid operation on all of $D$ , and the second from steps 2.1 and 2.2; nothing about $0$ is left implicit.
Why step 1.4 is not a triviality. "Every nonzero element is a unit" does not by itself say that the units are exactly the nonzero elements: the extra content is that $0$ is not a unit, and that needs $0 \cdot v = 0$ (In any ring $0 \cdot a = a \cdot 0 = 0$ , $(- a) b = a (- b) = - (a b)$ , $(- a) (- b) = a b$ , $(- 1) a = - a$ and $a (b - c) = a b - a c$ ) together with $1 \neq 0$ . In the one-element ring, where $1 = 0$ , the units are all of the ring and axiom (M) of Field would fail for want of $0 \neq 1$ .

Depends on

Used by

Subfield: a subring of a field closed under inverses of its nonzero elements, and therefore a field with the restricted operations Definition

Dependency tree · two levels

20 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Field (mathematics) (Wikipedia) (standard reference, not scraped)
Division ring (Wikipedia) (standard reference, not scraped)
Thomas W. Judson, Abstract Algebra: Theory and Applications, §16.4: Integral Domains and Fields (standard reference, not scraped)