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 finite module has the union of its generator-cyclic supports
Statement
If a left -module is generated by , then
Facts & Assumptions
Given: A commutative ring , a left -module , and generators of .
A prime ideal lies in exactly when for some (A prime lies in the support exactly when some element has annihilator inside it).
For an ideal , the support of is the set of primes containing (The support of a cyclic quotient is its vanishing set).
The generators generate every element of by finite -linear combinations (Generated submodule, cyclic and finitely generated modules, module basis and free module).
Proof
If , then because the empty list generates only the zero submodule. Both sides are therefore empty, so the formula holds. Hence assume .
Suppose . By [L1], choose with , and write using [L3]. If no were contained in , choose for every ; then because is prime, but , so , a contradiction. Thus for some , and [L2] gives .
Conversely, if for some , then [L2] gives , and [L1] applied to the element gives .
Steps 1.1, 1.2, and 1.3 prove the union formula.