TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

Eigenvectors belonging to pairwise distinct eigenvalues are linearly independent

Statement

Let $T : V \to V$ be linear. If $v_{1}, \dots, v_{m}$ are eigenvectors of $T$ belonging respectively to pairwise distinct eigenvalues $λ_{1}, \dots, λ_{m}$ , then $v_{1}, \dots, v_{m}$ are linearly independent.

Facts & Assumptions

Given: Eigenvectors $v_{1}, \dots, v_{m}$ of $T$ with pairwise distinct eigenvalues $λ_{1}, \dots, λ_{m}$ .

[L1]

An eigenvector is nonzero and satisfies $T (v_{i}) = λ_{i} v_{i}$ (Eigenvalues, eigenvectors, eigenspaces $E_{λ} (T) = \ker (T - λ I)$ , and the spectrum $σ_{F} (T)$ of an endomorphism).

[L2]

A finite family is linearly independent when every vanishing linear combination has all coefficients zero (Linear independence: a finite list $v : n \to V$ is independent when $\sum_{i < n} λ_{i} v_{i} = 0_{V}$ forces every $λ_{i} = 0_{F}$ , and a subset $S \subseteq V$ is independent when every injective finite list into $S$ is independent).

[F1]

Every nonzero element of a field has a multiplicative inverse (Field).

Proof

technique · induction on $m$

1.1

For $m = 0$ the empty family is independent, and for $m = 1$ the equation $a_{1} v_{1} = 0$ forces $a_{1} = 0$ because $v_{1} \neq 0$ .

baseL1L2F1

1.2

Assume $m \geq 2$ and that the claim holds for $m - 1$ eigenvectors. Suppose $\sum_{i = 1}^{m} a_{i} v_{i} = 0$ . Applying $T - λ_{m} I_{V}$ and using [L1] gives $\sum_{i = 1}^{m - 1} a_{i} (λ_{i} - λ_{m}) v_{i} = 0$ .

ihL1L2givenalgebra

2.1

The first $m - 1$ eigenvalues remain pairwise distinct, so the induction hypothesis gives $a_{i} (λ_{i} - λ_{m}) = 0$ for $i < m$ . Since $λ_{i} - λ_{m} \neq 0$ , [F1] gives $a_{i} = 0$ for every $i < m$ .

step 1.2ihF1given

3.1

The original relation now reads $a_{m} v_{m} = 0$ , so $a_{m} = 0$ by [L1] and [F1]. Thus the family is independent by [L2].

step 2.1L1L2F1

4.1

The base cases and induction step prove the claim for every finite family.

step 1.1step 3.1discharge-induction∎

Depends on

Used by

Dependency tree · two levels

13 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

S. Axler, Linear Algebra Done Right, 4th ed., Theorem 5.11 (standard reference, not scraped)