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.
A characteristic polynomial that splits into distinct linear factors forces diagonalisability
Statement
If the characteristic polynomial of a finite-dimensional endomorphism splits over into distinct linear factors, then the endomorphism is diagonalisable over .
Facts & Assumptions
Given: An endomorphism whose characteristic polynomial is a product of distinct linear factors over .
The minimal polynomial divides the characteristic polynomial (The minimal polynomial divides the characteristic polynomial, ).
An endomorphism is diagonalisable exactly when its minimal polynomial is a product of distinct linear factors (An endomorphism is diagonalisable if and only if its minimal polynomial is a product of distinct linear factors).
Splitting means factorisation into linear factors over the stated field, with repetitions allowed (Polynomials that split and splitting fields of a polynomial or a family of polynomials).
The polynomial ring over a field is a unique factorisation domain (For every field , is a unique factorisation domain).
Proof
By [L1], is a monic divisor of the split squarefree polynomial . Unique factorisation from [L4] and the meaning of splitting in [L3] therefore make a product of a subset of the same distinct linear factors.
Apply [L2] to step 1.1. The zero-dimensional case has and is included.
Depends on
- The minimal polynomial divides the characteristic polynomial, $\mu_T\mid\chi_T$
- An endomorphism is diagonalisable if and only if its minimal polynomial is a product of distinct linear factors
- Polynomials that split and splitting fields of a polynomial or a family of polynomials
- For every field $F$, $F[x]$ is a unique factorisation domain
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: 53 results over 8 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
- Sheldon Axler, Linear Algebra Done Right, 4th ed., §5D (standard reference, not scraped)