LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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.

A normal upper-triangular matrix is diagonal

Statement

Let $A = (a_{i j}) \in M_{n} (C)$ . If $A$ is upper triangular and normal, then $A$ is diagonal.

Facts & Assumptions

Given: An upper-triangular matrix $A = (a_{i j}) \in M_{n} (C)$ that is normal.

[L1]

A matrix is normal exactly when it 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.1

Because $A$ is upper triangular, the $n$ -th diagonal entry of $A A^{*}$ is $\sum_{j \geq n} ∣ a_{n j} ∣^{2} = ∣ a_{n n} ∣^{2}$ , while the $n$ -th diagonal entry of $A^{*} A$ is $\sum_{i \leq n} ∣ a_{i n} ∣^{2}$ ; [L1] makes these equal, so $a_{i n} = 0$ for every $i < n$ .

L1algebra

2.1

More generally, if every entry to the right of $a_{k k}$ in row $k$ is already zero, then the $k$ -th diagonal entries of $A A^{*}$ and $A^{*} A$ are $∣ a_{k k} ∣^{2}$ and $\sum_{i \leq k} ∣ a_{i k} ∣^{2}$ , so [L1] forces $a_{i k} = 0$ for every $i < k$ .

L1step 1.1algebra

3.1

Starting from $k = n$ in step 1.1 and descending through $k = n - 1, \dots, 1$ , step 2.1 shows that every entry above the diagonal is zero. Thus $A$ is diagonal.

step 1.1step 2.1∎

Depends on

In an orthonormal basis, self-adjoint means conjugate-transpose symmetry and normal means commuting with the conjugate transpose

Used by

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

Dependency tree · two levels

4 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Nicholas Hu, The Schur decomposition (standard reference, not scraped)