Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicableSession-authored (Fable 5 assisted)judge pass (z-ai/glm-5.2)audited 2026-07-28
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.

Division ring: a ring with 101 \ne 0 in which every nonzero element is a unit

Definition

A division ring (also skew field) is a ring DD (Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides) such that

Equivalently, D×=D{0}D^{\times} = D \setminus \{0\}: by (V2) every nonzero element is a unit, and by (V1) together with The units of a ring are the invertible elements of its multiplicative monoid, and R×R^{\times} is a group under multiplication; 0R×0 \in R^{\times} only in the zero ring the element 00 is not a unit, since 00 is a unit only when 1=01 = 0. Consequently (D{0},,1)(D \setminus \{0\}, \cdot, 1) is a group (The units of a ring are the invertible elements of its multiplicative monoid, and R×R^{\times} is a group under multiplication; 0R×0 \in R^{\times} only in the zero ring); in particular D{0}D \setminus \{0\} is closed under multiplication, so a division ring has no zero divisors.

A commutative division ring is a division ring whose multiplication is commutative. Those are exactly the fields (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, Every field is a commutative ring with 101 \ne 0; it is an integral domain, and it is a commutative division ring).

Remarks

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 16 results over 13 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources