TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11

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 square real matrix is invertible if and only if its determinant is nonzero

Statement

For every $n\ge1$ and every real matrix $A\in M_n(\mathbb R)$ , $A\text{ is invertible}\quad\Longleftrightarrow\quad\det(A)\ne0.$

Facts & Assumptions

Given: A real square matrix $A$ of positive finite size.

[L1]

Over a field, the ring-matrix and field-matrix interfaces agree (For a field, the ring-matrix operations, invertibility and similarity agree exactly with the established field-matrix interface).

[L2]

An $n\times n$ RREF with fewer than $n$ pivots has a zero row; its pivot columns increase from left to right (Row echelon form, reduced row echelon form, leading entries, pivots, pivot positions and pivot columns).

[L3]

A square matrix is invertible exactly when its RREF is the identity, equivalently when it has $n$ pivots (Invertible matrix theorem: invertibility, full pivot rank, RREF $I$ , trivial nullspace and unique solvability are equivalent).

[L4]

A row swap negates determinant, nonzero real row scaling multiplies it by a nonzero scalar, and row addition leaves it unchanged (For every square matrix, including singular ones, a row swap negates the determinant, scaling a row by any scalar scales it, and row addition leaves it unchanged).

[L5]

The determinant of a triangular matrix is the product of its diagonal entries (The determinant of a triangular matrix is the product of its diagonal entries).

[L6]

An invertible matrix over a commutative ring has unit determinant (An invertible square matrix over a commutative ring has unit determinant).

[L7]

The real numbers form a field (The reals form a field).

Proof

technique · direct

1.1

If $A$ is invertible, [L1] and [L6] make $\det(A)$ a unit of $\mathbb R$ , hence nonzero by [L7].

L1L6L7

1.2

Conversely suppose $A$ is not invertible and row reduce it to its RREF $R$ . By [L3], $R$ has fewer than $n$ pivots and hence a zero row. Its pivot in row $i$ , when present, lies in a column at least $i$ , so every entry below the diagonal is zero; thus $R$ is upper triangular.

L1L2L3

2.1

The zero row forces a zero diagonal entry, so [L5] gives $\det(R)=0$ .

step 1.2L5algebra

3.1

Along the finite real row reduction, swaps and row additions preserve whether determinant is zero, and a scaling uses a nonzero scalar whose inverse gives the reverse implication. Hence $\det(A)=0$ .

step 2.1L4L7algebra

4.1

Steps 1.2–3.1 prove the contrapositive $\det(A)\ne0\Rightarrow A$ invertible; combining it with step 1.1 proves the equivalence.

step 1.1step 3.1∎

Depends on

Used by

A linear endomorphism of ℝⁿ sends bounded Jordan sets to bounded Jordan sets and scales their content by the absolute determinant Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 99 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

D. Margalit and J. Rabinoff, Interactive Linear Algebra, §4.1, Invertibility Property (standard reference, not scraped)