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.

Every endomorphism of a nonzero finite-dimensional vector space over an algebraically closed field has an eigenvalue

Statement

Let $V$ be a nonzero finite-dimensional vector space over an algebraically closed field $F$ . Every endomorphism $T : V \to V$ has an eigenvalue in $F$ .

Facts & Assumptions

Given: A nonzero finite-dimensional $F$ -vector space $V$ , an algebraically closed field $F$ , and $T \in L (V)$ .

[L1]

Every nonconstant polynomial over an algebraically closed field has a root in that field (An algebraically closed field: every nonconstant polynomial has a root in the field).

[L2]

The characteristic polynomial of an endomorphism is by definition that of any representing matrix (The basis-independent characteristic polynomial $χ_{T}$ of an endomorphism of a finite-dimensional space, including $χ_{T} = 1$ in dimension zero), and for $A \in M_{n} (F)$ the polynomial $χ_{A} (x)$ is monic of degree $n$ ( $χ_{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$ ). So $χ_{T}$ is monic of degree $n = \dim V$ .

[L3]

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

Proof

technique · direct

1.1

Since $V \neq {0}$ , its finite dimension $n$ is positive, so [L2] makes $χ_{T}$ a nonconstant polynomial.

L2given

2.1

By [L1], $χ_{T}$ has a root $λ \in F$ , and [L3] makes $λ$ an eigenvalue of $T$ .

step 1.1L1L3

3.1

Hence every such endomorphism has an eigenvalue; the excluded zero-dimensional case would have characteristic polynomial $1$ and no eigenvalue.

step 2.1L2L3∎

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: 49 results over 10 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

M. Khovanov, Linear Algebra II notes, §6 (standard reference, not scraped)