CorollaryStatement: Literature-sourcedProof: 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.

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

Statement

Let $F$ be a field, $n \geq 1$ , $A \in M_{n} (F)$ , and fix $b \in F^{n}$ . The system $A x = b$ has a unique solution if and only if $\det (A) \neq 0$ . In that case

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

Facts & Assumptions

Given: $F, n, A, b$ as in the statement.

[F1]

A field is a commutative ring, and every nonzero field element is a unit (Every field is a commutative ring with $1 \neq 0$ ; it is an integral domain, and it is a commutative division ring).

[L1]

Over a commutative ring, a unit determinant gives the unique Cramer solution $x_{j} = \det (A)^{- 1} \det (A_{j} (b))$ (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).

[L2]

A square matrix over a field is invertible exactly when its kernel is zero (Invertible matrix theorem: invertibility, full pivot rank, RREF $I$ , trivial nullspace and unique solvability are equivalent).

[L3]

A positive-sized square matrix over a commutative ring is invertible exactly when its determinant is a unit (A positive-sized square matrix over a commutative ring is invertible if and only if its determinant is a unit).

[L4]

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

Proof

technique · direct

1.1

If $\det (A) \neq 0$ , it is a unit by [F1], so [L1] gives the unique solution and the displayed quotient formula.

F1L1

1.2

Conversely, suppose $A x = b$ has the unique solution $x$ . If $A z = 0$ , then $A (x + z) = b$ by distributivity, so uniqueness gives $z = 0$ . Thus the kernel of $A$ is zero.

L4given

2.1

By [L2], step 1.2 makes $A$ invertible. By [L3] and [F1], $\det (A)$ is a unit and hence is nonzero.

step 1.2L2L3F1

3.1

Steps 1.1 and 2.1 prove both directions.

step 1.1step 2.1∎

Depends on

Used by

Cramer's rule solves 2x+y=5 and x-y=1 as (x,y)=(2,1) Example

Dependency tree · next 3 levels

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

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