LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (openai/gpt-5.4)audited 2026-07-25

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.

A field has no zero divisors: $ab = 0 \Rightarrow a = 0$ or $b = 0$

Statement

In any field $F$ (Field), if $a, b \in F$ satisfy $ab = 0$ , then $a = 0$ or $b = 0$ .

Facts & Assumptions

Given: A field $F$ and elements $a, b \in F$ with $ab = 0$ .

[L1]

Field axioms (Field): if $a \ne 0$ then $a$ has a multiplicative inverse $a^{-1}$ with $a^{-1} a = 1$ ; multiplication is associative; and $1$ is the multiplicative identity, so $1 \cdot x = x$ .

[L2]

For every $x \in F$ , $x \cdot 0 = 0$ (Multiplication by zero: $0 \cdot a = 0$ , using commutativity).

Proof

technique · direct

1.1

If $a = 0$ the disjunction $a = 0$ or $b = 0$ already holds, so it suffices to assume $a \ne 0$ and derive $b = 0$ .

suffices: a ne 0 implies b = 0

1.2

Assuming $a \ne 0$ , the inverse $a^{-1}$ exists with $a^{-1} a = 1$ .

1.3

Since $1$ is the multiplicative identity, $b = 1 \cdot b$ .

1.4

By associativity, $(a^{-1} a) \cdot b = a^{-1} (a b)$ .

1.5

We are given $ab = 0$ .

given

1.6

$a^{-1} \cdot 0 = 0$ .

2.1

Substituting $1 = a^{-1} a$ into $b = 1 \cdot b$ and using associativity gives $b = (a^{-1} a) b = a^{-1}(ab)$ .

step 1.2step 1.3step 1.4

2.2

Since $ab = 0$ , we have $a^{-1}(ab) = a^{-1} \cdot 0$ .

step 1.5

3.1

Combining, $b = a^{-1}(ab) = a^{-1} \cdot 0 = 0$ .

step 2.1step 2.2step 1.6

4.1

Hence $a \ne 0$ forces $b = 0$ , so in every case $a = 0$ or $b = 0$ .

step 1.1step 3.1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 2 results over 2 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

W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (standard reference, not scraped)
M. Spivak, Calculus, 4th ed., Ch. 1 (standard reference, not scraped)
Tom Denton, Introduction to Algebraic Structures: The Problem of Division (standard reference, not scraped)

A field has no zero divisors: ab=0⇒a=0ab = 0 \Rightarrow a = 0ab=0⇒a=0 or b=0b = 0b=0