CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17

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.

Integral elements over a nonzero base ring form a subring

Statement

Let $A \subseteq B$ be commutative rings with $A \neq 0$ . The elements of $B$ integral over $A$ form a subring of $B$ . See Integrality and finite-module characterizations for one element.

Facts & Assumptions

Given: The hypotheses and objects in the Statement.

[L1]

Let $A \subseteq B$ be commutative rings with $A \neq 0$ , and let $b \in B$ . Then $b$ is integral over $A$ if and only if $A [b]$ is finitely generated as an $A$ -module, if and only if there exists a faithful $A [b]$ -module that is finitely generated over $A$ . (Integrality and finite-module characterizations for one element).

[L2]

Let $A \to B$ be a homomorphism of commutative rings. An element $b \in B$ is integral over $A$ when it is a root of a monic polynomial in $A [X]$ . The extension is integral when every element is integral. An algebraic integer is a complex number integral over $Z$ . (Integral elements over a commutative ring and algebraic integers).

Proof

technique · direct

1.1

If $x, y$ are integral, $A [x]$ is finite over $A$ , and the monic equation for $y$ over $A$ is also one over $A [x]$ ; multiplying finite generating sets shows that $A [x, y]$ is finite over $A$ .

L1L2givenalgebra

2.1

For each $z \in {x + y, x - y, x y}$ , the $A [z]$ -module $A [x, y]$ is faithful and finite over $A$ , so the finite-module criterion makes $z$ integral.

step 1.1givenalgebra

3.1

The elements $0$ and $1$ are roots of the monic polynomials $X$ and $X - 1$ , respectively; step 2.1 supplies closure under addition, multiplication, and additive inverses, including coincident elements. Thus the integral elements form a unital subring of $B$ .

L2step 2.1givenalgebra∎

Depends on

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: 18 results over 5 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

Eloisa Grifo, Commutative Algebra I, Section 1.4 (standard reference, not scraped)