TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16

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.

The characteristic of a field is zero or a prime number

Statement

The characteristic of a field is either $0$ or a prime number.

Facts & Assumptions

Given: A field $F$ .

[L1]

If the set of positive $n$ with $n \cdot 1_{F} = 0$ is nonempty, the characteristic is its least element; otherwise it is $0$ (The characteristic of a ring: the least $n \geq 1$ with $n \cdot 1_{R} = 0$ when one exists, and $0$ otherwise).

[L2]

A natural number greater than $1$ is prime exactly when it has no factorization into two natural numbers strictly between $1$ and itself (Prime and composite integers: $p$ is prime when $p > 1$ and its only positive divisors are $1$ and $p$ ).

[L3]

A field is an integral domain, so a product of two nonzero elements cannot be zero (Every field is a commutative ring with $1 \neq 0$ ; it is an integral domain, and it is a commutative division ring).

Proof

technique · contradiction

1.1

If no positive multiple of $1_{F}$ is zero, [L1] gives characteristic $0$ . Otherwise write $n = char F$ . Since $1_{F} \neq 0$ , one has $n > 1$ .

givenL1

2.1

Suppose, for contradiction, that this positive $n$ is not prime. By [L2], write $n = a b$ with $1 < a < n$ and $1 < b < n$ .

step 1.1L2assume-contra

3.1

Minimality of $n$ gives $a \cdot 1_{F} \neq 0$ and $b \cdot 1_{F} \neq 0$ , while their product is $(a b) \cdot 1_{F} = n \cdot 1_{F} = 0$ . This contradicts [L3].

step 1.1step 2.1L1L3algebra

4.1

Therefore the positive characteristic is prime, completing both cases.

step 3.1discharge-contradiction∎

Depends on

Used by

Dependency tree · next 3 levels

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

A. W. Knapp, Basic Algebra, 2nd ed., Chapter IX, Section 3 (standard reference, not scraped)