TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16

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 family of diagonalisable endomorphisms of a finite-dimensional space is simultaneously diagonalisable if and only if its members commute pairwise

Statement

Let $T$ be a family of diagonalisable endomorphisms of a finite-dimensional vector space. Then $T$ is simultaneously diagonalisable if and only if its members commute pairwise.

Facts & Assumptions

Given: A family $T$ of diagonalisable endomorphisms of a finite-dimensional space $V$ .

[L1]

Commuting endomorphisms preserve each other's eigenspaces (Commuting endomorphisms preserve each other's eigenspaces).

[L2]

The restriction of a diagonalisable endomorphism to an invariant subspace is diagonalisable (The restriction of a diagonalisable endomorphism to an invariant subspace is diagonalisable).

[L3]

The space $L (V, V)$ is finite-dimensional, with dimension $(\dim V)^{2}$ ( $\dim_{F} M_{m \times n} (F) = m n$ and $\dim_{F} L (V, W) = (\dim_{F} V) (\dim_{F} W)$ for finite-dimensional $V, W$ ).

[L4]

$span (S)$ is the intersection of all subspaces containing $S$ , hence the smallest such subspace (Linear combination of a finite list, and the span $span (S)$ as the smallest linear subspace containing $S$ ); and $span (S) = L (S)$ , the set of finite linear combinations of elements of $S$ ( $span (S)$ is exactly the set of linear combinations of finite lists of elements of $S$ , and $span (\emptyset) = {0_{V}}$ ).

[L5]

A diagonalisable endomorphism's distinct eigenspaces have direct sum equal to the whole space (An endomorphism is diagonalisable exactly when $V = ⨁_{i < r} E_{λ_{i}} (T)$ for some finite list of distinct scalars $λ_{i}$ ).

[L6]

Simultaneous diagonalisability means that one basis diagonalises every member of the family (Simultaneous diagonalisability: one basis that diagonalises every endomorphism in a family).

Proof

technique · direct

1.1

First suppose $T$ is finite and pairwise commuting. Induct on its size. For the empty family any basis works. For a nonempty family, choose one member $T$ . Its eigenspaces have direct sum $V$ by [L5]; by [L1] every remaining member preserves each eigenspace, and by [L2] every restriction is diagonalisable. Applying the induction hypothesis within each eigenspace and concatenating the resulting bases gives one common eigenbasis.

L1L2L5choose

1.2

For an arbitrary pairwise commuting family, [L3] makes $U = span (T)$ finite-dimensional. Choose a finite basis of $U$ ; by [L4], each basis vector is a finite linear combination of members of $T$ . The union of the finitely many supports is a finite subfamily $T_{0}$ spanning $U$ .

L3L4choose

1.3

Conversely, if one basis diagonalises every member of $T$ as in [L6], then every pair is represented by diagonal matrices, which commute. The represented endomorphisms therefore commute.

L6givenalgebra

2.1

Step 1.1 gives a common eigenbasis for $T_{0}$ . Every member of $T$ lies in its span, so it is represented by a linear combination of diagonal matrices in that basis and is diagonal too. Hence [L6] makes $T$ simultaneously diagonalisable.

step 1.1step 1.2L6

3.1

Steps 2.1 and 1.3 prove both directions, including empty families and the zero space.

step 2.1step 1.3∎

Depends on

Used by

Dependency tree · next 3 levels

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

Keith Conrad, The Minimal Polynomial and Some Applications, Theorem 5.2 and Corollary 5.4 (standard reference, not scraped)