TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28

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.

Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely

Statement

Let $V$ be a finite-dimensional complex inner product space and let $T : V \to V$ be linear. Then $T$ is normal if and only if $V$ has an orthonormal basis consisting of eigenvectors of $T$ .

Facts & Assumptions

Given: A finite-dimensional complex inner product space $V$ and a linear endomorphism $T : V \to V$ .

[L1]

The field $C$ is algebraically closed (The complex numbers are algebraically closed).

[L2]

If the characteristic polynomial splits, then some orthonormal basis makes the matrix upper triangular (If the characteristic polynomial of an endomorphism splits, some orthonormal basis makes its matrix upper triangular).

[L3]

A normal upper-triangular complex matrix is diagonal (A normal upper-triangular matrix is diagonal).

[L4]

In an orthonormal basis, a linear map is normal exactly when its matrix commutes with its conjugate transpose (In an orthonormal basis, self-adjoint means conjugate-transpose symmetry and normal means commuting with the conjugate transpose).

Proof

technique · direct

1.1L1L2L3L4

Assume $T$ is normal. By [L1], the characteristic polynomial of $T$ splits over $C$ , so [L2] gives an orthonormal basis in which the matrix of $T$ is upper triangular. Because $T$ is normal, [L4] makes that matrix normal, and then [L3] makes it diagonal. Hence the chosen orthonormal basis consists of eigenvectors of $T$ .

2.1L4algebra∎

Conversely, assume $(e_{1}, \dots, e_{n})$ is an orthonormal basis of eigenvectors of $T$ , with $T e_{j} = λ_{j} e_{j}$ . Then the matrix of $T$ in that basis is the diagonal matrix $diag (λ_{1}, \dots, λ_{n})$ , and every diagonal matrix commutes with its conjugate transpose. By [L4], $T$ is normal.

Depends on

Dependency tree · 2 levels

Sources

Sheldon Axler, Linear Algebra Done Right, fourth edition