ExampleConstruction: AI-generatedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 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.

The ring $(Z / 2)^{N}$ is not Noetherian

Example

The product ring $R = (Z / 2)^{N}$ is not Noetherian: its ideals generated by the first finitely many coordinate idempotents form a strict ascending chain. See Left and right Noetherian rings.

Facts & Assumptions

Given: The hypotheses and objects in the Example.

[L1]

A unital ring $R$ is left Noetherian when its left regular module $_{R} R$ is Noetherian, and right Noetherian when the right regular module $R_{R}$ is Noetherian. Unqualified “Noetherian ring” means left Noetherian here; the side is stated whenever both notions occur. (Left and right Noetherian rings).

[L2]

Let $R$ be a unital ring and $(M_{i})_{i \in I}$ a family of left $R$ -modules (def-left-and-right-modules). Their direct product is the module $\prod_{i \in I} M_{i}$ with coordinatewise operations. The support of $m = (m_{i})$ is ${i \in I : m_{i} \neq 0}$ , and the direct sum is the submodule $⨁_{i \in I} M_{i} = {m \in \prod_{i \in I} M_{i} : supp (m) is finite}$ (def-submodule). (The direct sum of an indexed family of modules).

[L3]

For every $n \in N$ , with addition and multiplication as in def-addition-and-multiplication-modulo-n: 1. $(Z / n, +, [0]_{n})$ is an abelian group (def-group), with $- [a]_{n} = [- a]_{n}$ ; 2. $(Z / n, \cdot, [1]_{n})$ is a commutative monoid (def-semigroup-and-monoid); 3. multiplication distributes over addition on both sides. (For every natural $n$ , $(Z / n, +)$ is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold).

Verification

technique · direct

1.1

In $R = (Z / 2)^{N}$ , let $e_{i}$ have value $1$ in coordinate $i$ and $0$ elsewhere, and set $I_{n} = R e_{0} + \dots + R e_{n}$ . Then $I_{n}$ consists exactly of the sequences supported in ${0, \dots, n}$ .

L1L2L3givenalgebra

2.1

Since $e_{n + 1} \in I_{n + 1} ∖ I_{n}$ , the chain $I_{0} < I_{1} < I_{2} < \dots$ is strictly ascending; hence the regular module is not Noetherian.

step 1.1givenalgebra

3.1

The union $⋃_{n} I_{n}$ is only the finite-support ideal; for example the multiplicative identity $(1, 1, \dots)$ belongs to the product ring but not to that union. Thus the witness is genuinely an ideal chain in the full product ring. This proves the stated claim.

step 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: 31 results over 13 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.

The ring (Z/2)N(Z/2)N is not Noetherian