TheoremStatement: 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.

A finite-dimensional linear operator over a field is invertible if and only if its determinant is nonzero

Statement

Let $T : V \to V$ be a linear operator on a finite-dimensional vector space over a field $F$ . Then $T$ is invertible if and only if $\det (T) \neq 0$ .

Facts & Assumptions

Given: $T, V, F$ as in the statement.

[L1]

If $T$ is invertible, its representing matrix is invertible (A square matrix is invertible exactly when its multiplication map is a linear isomorphism; matrices preserve inverses of linear isomorphisms).

[L4]

Every square matrix is the representing matrix of a unique operator, and composition of operators becomes multiplication of their matrices ( $T \mapsto [T]_{B}^{C}$ is a vector-space isomorphism $L (V, W) ≅ M_{m \times n} (F)$ , $[S \circ T]_{B}^{D} = [S]_{C}^{D} [T]_{B}^{C}$ ).

[L2]

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).

[F1]

A field is a commutative ring and its units are precisely its nonzero elements (Every field is a commutative ring with $1 \neq 0$ ; it is an integral domain, and it is a commutative division ring).

[L3]

The operator determinant is the determinant of a representing matrix and is basis independent (The determinant of a linear operator is independent of the chosen ordered basis).

[F2]

In dimension zero, the operator determinant is defined to be $1$ (The determinant of an endomorphism of a finite-dimensional vector space: its matrix determinant in an ordered basis in positive dimension, and $1$ on the zero space).

Proof

technique · direct

1.1

Suppose $\dim V \geq 1$ and choose an ordered basis, writing $A = [T]$ . If $T$ is invertible, then $A$ is invertible by [L1]. Conversely, if $A$ is invertible, [L4] gives an operator $S$ with $[S] = A^{- 1}$ ; the composite formula gives $[S \circ T] = I = [T \circ S]$ , and injectivity of matrix representation gives $S \circ T = I_{V} = T \circ S$ . Thus $T$ is invertible exactly when $A$ is invertible.

L1L4algebra

1.2

If $\dim V = 0$ , the unique endomorphism is the identity and is invertible, while [F2] gives $\det (T) = 1 \neq 0$ .

F2algebra

2.1

By [L2] and [F1], $A$ is invertible exactly when $\det (A) \neq 0$ ; by [L3], this is exactly $\det (T) \neq 0$ .

step 1.1L2F1L3

3.1

Steps 2.1 and 1.2 establish the equivalence in every finite dimension.

step 2.1step 1.2∎

Depends on

Used by

Dependency tree · next 3 levels

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

Sheldon Axler, Linear Algebra Done Right, 4th ed. (standard reference, not scraped)