CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

If $χ_{T}$ splits over $F$ , every eigenvalue of $χ_{T} (T)$ is $0$

Statement

Let $T$ be a finite-dimensional endomorphism whose characteristic polynomial splits over $F$ . Every eigenvalue of $χ_{T} (T)$ is $0$ .

Facts & Assumptions

Given: A finite-dimensional endomorphism $T$ for which $χ_{T}$ splits over $F$ .

[L1]

If $χ_{T} (x) = \prod_{i < n} (x - λ_{i})$ , then $χ_{p (T)} (y) = \prod_{i < n} (y - p (λ_{i}))$ (If $χ_{T} (x) = \prod_{i < n} (x - λ_{i})$ in $F [x]$ , then $χ_{p (T)} (y) = \prod_{i < n} (y - p (λ_{i}))$ for every $p \in F [x]$ : the eigenvalues of $p (T)$ are $p (λ_{i})$ , counted with algebraic multiplicity).

[L2]

In dimension zero, $χ_{T} = 1$ (The basis-independent characteristic polynomial $χ_{T}$ of an endomorphism of a finite-dimensional space, including $χ_{T} = 1$ in dimension zero).

[L3]

The eigenvalues of an operator are exactly the roots of its characteristic polynomial (For every finite-dimensional space, $σ_{F} (T)$ is exactly the set of roots in $F$ of $χ_{T}$ ).

Proof

technique · direct

1.1

If $\dim V = 0$ , the spectrum of every endomorphism is empty, so the assertion is vacuous; [L2] also gives the correct empty factorization.

L2L3

1.2

Otherwise write $χ_{T} (x) = \prod_{i < n} (x - λ_{i})$ . Each $λ_{i}$ is a root, so $χ_{T} (λ_{i}) = 0$ . Applying [L1] with $p = χ_{T}$ gives $χ_{χ_{T} (T)} (y) = \prod_{i < n} (y - 0) = y^{n}$ .

L1givenalgebra

2.1

By [L3], the only possible root, and hence the only possible eigenvalue, is $0$ . Together with step 1.1 this proves the claim.

step 1.1step 1.2L3∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

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

H. Pinkham, Linear Algebra, §12.3.4 (standard reference, not scraped)

If χTχT​ splits over FF, every eigenvalue of χT(T)χT​(T) is 00