TheoremStatement: AI-adaptedProof: 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} (x) = \prod_{i < n} (x - λ_{i})$ in $F [x]$ , then $tr (T) = \sum_{i < n} λ_{i}$ : trace is the sum of the eigenvalues counted with algebraic multiplicity

Statement

Let $T$ be an endomorphism of an $n$ -dimensional vector space over $F$ . If

$χ_{T} (x) = \prod_{i < n} (x - λ_{i})$

in $F [x]$ , then $tr (T) = \sum_{i < n} λ_{i}$ . Thus the trace is the sum of the eigenvalues counted with algebraic multiplicity.

Facts & Assumptions

Given: $T$ as stated and a displayed factorization $χ_{T} (x) = \prod_{i < n} (x - λ_{i})$ .

[L1]

The operator characteristic polynomial is the characteristic polynomial of any representing matrix, including value $1$ in dimension zero (The basis-independent characteristic polynomial $χ_{T}$ of an endomorphism of a finite-dimensional space, including $χ_{T} = 1$ in dimension zero).

[L2]

In positive size, the coefficient of $x^{n - 1}$ in a characteristic polynomial is the negative of the matrix trace ( $χ_{A} (x)$ is monic of degree $n$ ; for $n \geq 1$ its $x^{n - 1}$ coefficient is $- tr (A)$ and its constant coefficient is $(- 1)^{n} \det (A)$ , while $χ_{0 \times 0} = 1$ ).

[L3]

The trace of an endomorphism is the trace of any representing matrix and is $0$ in dimension zero (The basis-independent trace of an endomorphism of a finite-dimensional vector space).

[L4]

Roots of $χ_{T}$ are precisely eigenvalues (For every finite-dimensional space, $σ_{F} (T)$ is exactly the set of roots in $F$ of $χ_{T}$ ), and algebraic multiplicity is the exponent of the corresponding linear factor (Algebraic multiplicity as the exponent of $x - λ$ in $χ_{T}$ , and geometric multiplicity as $\dim E_{λ} (T)$ ).

Proof

technique · direct

1.1

If $n = 0$ , [L3] gives $tr (T) = 0$ , while the sum indexed by the empty set is $0$ .

L1L3algebra

1.2

Suppose $n \geq 1$ . By [L1]–[L3], the coefficient of $x^{n - 1}$ in $χ_{T}$ is $- tr (T)$ . In the given product, obtaining degree $n - 1$ means choosing $- λ_{i}$ from exactly one factor, so the same coefficient is $- \sum_{i < n} λ_{i}$ .

L1L2L3givenalgebra

2.1

Equality of coefficients and additive cancellation give $tr (T) = \sum_{i < n} λ_{i}$ . By [L4], the factors list exactly the eigenvalues with their algebraic multiplicities.

step 1.2L4algebra

3.1

Steps 1.1 and 2.1 prove the formula in every finite dimension.

step 1.1step 2.1∎

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: 75 results over 13 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.1 (standard reference, not scraped)

If χT(x)=∏i<n(x−λi)χT​(x)=∏i<n​(x−λi​) in F[x]F[x], then tr⁡(T)=∑i<nλitr(T)=∑i<n​λi​: trace is the sum of the eigenvalues counted with algebraic multiplicity