Alphabeta MathHow 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.
For every finite-dimensional space, is exactly the set of roots in of
Statement
For an endomorphism of a finite-dimensional -vector space,
Facts & Assumptions
Given: A finite-dimensional -vector space and .
In any basis, is the characteristic polynomial of the representing matrix; in dimension zero it is (The basis-independent characteristic polynomial of an endomorphism of a finite-dimensional space, including in dimension zero).
A scalar is an eigenvalue exactly when is not invertible (For a finite-dimensional space, is an eigenvalue of if and only if is not invertible).
A finite-dimensional endomorphism is invertible exactly when its determinant is nonzero (A finite-dimensional linear operator over a field is invertible if and only if its determinant is nonzero).
A root of a polynomial is a scalar at which its evaluation is zero (Evaluation and roots of a polynomial in a commutative target ring).
Proof
If , the spectrum is empty because there is no nonzero eigenvector, while [L1] gives , which has no root.
Suppose and choose a basis with matrix . Then .
The scalar is nonzero. Thus step 1.2, [L3], and [L2] give if and only if is not invertible if and only if .
Steps 1.1 and 2.1 prove the set equality in every finite dimension and prove both directions of the equivalence.
Depends on
- The basis-independent characteristic polynomial $\chi_T$ of an endomorphism of a finite-dimensional space, including $\chi_T=1$ in dimension zero
- For a finite-dimensional space, $\lambda$ is an eigenvalue of $T$ if and only if $T-\lambda I$ is not invertible
- A finite-dimensional linear operator over a field is invertible if and only if its determinant is nonzero
- Evaluation and roots of a polynomial in a commutative target ring
Used by
- Every endomorphism of a nonzero finite-dimensional vector space over an algebraically closed field has an eigenvalue Corollary
- If χ_T splits over F, every eigenvalue of χ_T(T) is 0 Corollary
- A quarter-turn of ℝ² has characteristic polynomial x²+1 and no real eigenvalue Example
- beginpmatrix0&11&1 endpmatrix over F₂ has characteristic polynomial x²+x+1 and no eigenvalue in its base field Example
- If χ_T(x)=∏_i<n(x-λᵢ) in F[x], then det(T)=∏_i<nλᵢ: determinant is the product of the eigenvalues counted with algebraic multiplicity Theorem
- If χ_T(x)=∏_i<n(x-λᵢ) in F[x], then tr(T)=∑_i<nλᵢ: trace is the sum of the eigenvalues counted with algebraic multiplicity Theorem
- If χ_T(x)=∏_i<n(x-λᵢ) in F[x], then χ_p(T)(y)=∏_i<n(y-p(λᵢ)) for every p∈ F[x]: the eigenvalues of p(T) are p(λᵢ), counted with algebraic multiplicity Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 83 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
- M. Khovanov, Linear Algebra II notes, §6 (standard reference, not scraped)