LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16

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.

Formally, $(I - x A)^{- 1} = \sum_{n \geq 0} A^{n} x^{n}$ over every commutative coefficient ring

Statement

Let $R$ be a commutative ring, let $p \in N$ , and let $A \in M_{p} (R)$ . In the matrix ring $M_{p} (R ⟦ x ⟧)$ ,

$(I_{p} - x A)^{- 1} = \sum_{n \geq 0} A^{n} x^{n} .$

The matrix series is defined entrywise. The identity is formal, including $p = 0$ , and uses no norm, convergence, or spectral-radius hypothesis.

Facts & Assumptions

Given: A commutative ring $R$ , a size $p \in N$ , and a matrix $A \in M_{p} (R)$ .

[L1]

Formal series are coefficient functions with Cauchy product $[x^{n}] (f g) = \sum_{i = 0}^{n} [x^{i}] f [x^{n - i}] g$ (Formal power series over a commutative ring and the coefficient-extraction functional $[x^{n}]$ ).

[L2]

Cauchy multiplication makes $R ⟦ x ⟧$ a commutative ring containing $R [x]$ (Cauchy multiplication makes $R ⟦ x ⟧$ a commutative ring containing $R [x]$ as the finitely supported subring).

[L3]

Matrix products use finite row-column sums and $I_{p}$ is the identity matrix (Entrywise ring-matrix operations, rectangular matrix products, identity matrices and transpose).

[L4]

Matrix multiplication is associative and distributive, including zero-sized shapes (Matrix arithmetic over a commutative ring is associative, unital and distributive, and transpose reverses products).

Proof

technique · direct

1.1givenL1L2L3L4

Define $S = \sum_{n \geq 0} A^{n} x^{n}$ entrywise. The constant coefficient of $(I_{p} - x A) S$ is $I_{p}$ , and for every $n \geq 1$ its coefficient is $A^{n} - A A^{n - 1} = 0$ .

1.2givenL1L2L3L4

The same coefficient calculation on the other side gives the constant coefficient $I_{p}$ and positive coefficient $A^{n} - A^{n - 1} A = 0$ for $S (I_{p} - x A)$ .

2.1step 1.1step 1.2L1∎

Coefficient extensionality makes both products equal to $I_{p}$ , so $S$ is the two-sided inverse of $I_{p} - x A$ . For $p = 0$ all matrices are the unique empty matrix and the same identity holds.

Depends on

Used by

Dependency tree · two levels

12 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

R. P. Stanley, Enumerative Combinatorics, vol. 1, 2nd ed., Theorem 4.7.2 (standard reference, not scraped)

Formally, (I−xA)−1=∑n≥0Anxn(I−xA)−1=∑n≥0​Anxn over every commutative coefficient ring