LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27

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.

Vanishing sets of arbitrary sums

Statement

Let $R$ be a commutative ring, and let $(I_{λ})_{λ \in Λ}$ be a family of ideals of $R$ . Write $\sum_{λ \in Λ} I_{λ}$ for the ideal of finite sums of elements drawn from the family, with the empty sum equal to $0$ . Then $V ⁣ (\sum_{λ \in Λ} I_{λ}) = ⋂_{λ \in Λ} V (I_{λ}) .$

Facts & Assumptions

Given: A commutative ring $R$ and a family $(I_{λ})_{λ \in Λ}$ of ideals of $R$ .

[L1]

$V (K)$ is the set of prime ideals containing the ideal $K$ (The prime spectrum and vanishing sets).

Proof

technique · direct

1.1L1given

If $p \in V ⁣ (\sum_{λ} I_{λ})$ , then $\sum_{λ} I_{λ} \subseteq p$ . Since every $I_{λ}$ is contained in that sum, one has $I_{λ} \subseteq p$ for every $λ$ , so $p \in V (I_{λ})$ for all $λ$ .

1.2L1givenalgebra

Conversely, if $p \in V (I_{λ})$ for every $λ$ , then each $I_{λ}$ lies in $p$ . Because $p$ is an ideal, it contains every finite sum of elements coming from the family, hence it contains $\sum_{λ} I_{λ}$ . Therefore $p \in V ⁣ (\sum_{λ} I_{λ})$ .

Vanishing sets of arbitrary sums

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources