TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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.

Cramer's rule over a commutative ring: every solution satisfies $\det (A) x_{j} = \det (A_{j} (b))$ , and a unit determinant gives the unique quotient formula

Statement

Let $R$ be a commutative ring, $n \geq 1$ , $A \in M_{n} (R)$ , and $b \in R^{n}$ . Let $A_{j} (b)$ be obtained from $A$ by replacing column $j$ by $b$ . Every solution $x$ of $A x = b$ satisfies

$\det (A) x_{j} = \det (A_{j} (b)) (0 \leq j < n) .$

If $\det (A)$ is a unit, the solution is unique and

$x_{j} = \det (A)^{- 1} \det (A_{j} (b)) .$

Facts & Assumptions

Given: $R, n, A, b, j$ as in the statement, and a solution $x$ when the first claim is used.

[L1]

The determinant is alternating and multilinear in columns (The Leibniz determinant is column-multilinear, alternating and normalized over every commutative ring).

[L2]

Laplace expansion along a column computes the determinant as the sum of its entries times their cofactors (Laplace expansion computes the determinant along every row and every column over a commutative ring).

[L3]

If $\det (A)$ is a unit, then $A$ is invertible (A positive-sized square matrix over a commutative ring is invertible if and only if its determinant is a unit) and $A^{- 1} = \det (A)^{- 1} adj (A)$ (If $\det (A)$ is a unit, then $A^{- 1} = \det (A)^{- 1} adj (A)$ ).

[F1]

Matrix multiplication obeys the entry formula (Entrywise ring-matrix operations, rectangular matrix products, identity matrices and transpose).

[L4]

Matrix multiplication is associative and distributive (Matrix arithmetic over a commutative ring is associative, unital and distributive, and transpose reverses products).

Proof

technique · direct

1.1

If $A x = b$ , then $b = \sum_{k} x_{k} A_{k}$ , where $A_{k}$ is column $k$ of $A$ .

F1given

1.2

Now suppose $u : = \det (A)$ is a unit. By [L3], $A$ is invertible, so $x = A^{- 1} b = u^{- 1} adj (A) b$ is the unique solution.

L3L4

2.1

Replace column $j$ by the sum from step 1.1 and use column multilinearity. Every term with $k \neq j$ has two equal columns and vanishes; the term $k = j$ is $x_{j} \det (A)$ . Thus $\det (A_{j} (b)) = x_{j} \det (A)$ .

step 1.1L1

2.2

Its $j$ th coordinate is $u^{- 1} \sum_{i} C_{i j} (A) b_{i}$ . Deleting column $j$ removes the replaced column, so $C_{i j} (A_{j} (b)) = C_{i j} (A)$ ; expanding $A_{j} (b)$ along column $j$ therefore identifies the sum as $\det (A_{j} (b))$ .

step 1.2F1L2

3.1

Step 2.1 proves the unconditional cross-multiplied identity, and step 2.2 proves the quotient formula and uniqueness under the unit hypothesis.

step 2.1step 2.2∎

Depends on

Used by

Over a field, for each right-hand side b, Ax=b has a unique solution exactly when det(A) is nonzero, and then Cramer's quotient formula holds Corollary

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 54 results over 16 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

Interactive Linear Algebra (standard reference, not scraped)
András Pál, Introduction to Commutative Algebra (standard reference, not scraped)

Cramer's rule over a commutative ring: every solution satisfies det⁡(A)xj=det⁡(Aj(b))det(A)xj​=det(Aj​(b)), and a unit determinant gives the unique quotient formula