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

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.

Assuming the Axiom of Choice, a local ring has no idempotents other than $0$ and $1$

Statement

Assume the Axiom of Choice. If $R$ is a local ring and $e \in R$ satisfies $e^{2} = e$ , then $e = 0$ or $e = 1$ .

Facts & Assumptions

Given: A local ring $R$ and an idempotent $e \in R$ .

[F1]

For every element $x$ of a local ring, at least one of $x$ and $1 - x$ is a unit (Assuming the Axiom of Choice, a nonzero commutative ring is local exactly when its nonunits form an ideal, exactly when one of $x$ and $1 - x$ is a unit for every $x$ ).

Proof

technique · cases

1.1

By [F1], either $e$ is a unit or $1 - e$ is a unit. If $e$ is a unit, multiplying $e^{2} = e$ by $e^{- 1}$ gives $e = 1$ .

F1algebraassume-case eunit

2.1

If $1 - e$ is a unit, then $(1 - e) e = e - e^{2} = 0$ ; multiplying by $(1 - e)^{- 1}$ gives $e = 0$ . The two cases prove the claim, including the endpoint idempotents themselves.

F1algebraassume-case complementcases-exhaustive∎

Depends on

Assuming the Axiom of Choice, a nonzero commutative ring is local exactly when its nonunits form an ideal, exactly when one of $x$ and $1-x$ is a unit for every $x$

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

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

The Stacks Project, Section 10.18: Local rings (standard reference, not scraped)

Assuming the Axiom of Choice, a local ring has no idempotents other than 00 and 11