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.
Similar matrices have the same characteristic polynomial
Statement
If are similar, then in , including .
Facts & Assumptions
Given: Similar matrices .
Similarity means that for some invertible (Similar matrices: for an invertible ).
For positive size over a commutative ring, (For same-sized finite square matrices over a commutative ring, ).
Field matrices embed entrywise into matrices over , with the same matrix arithmetic and determinant (For a field, the ring-matrix operations, invertibility and similarity agree exactly with the established field-matrix interface).
The characteristic polynomial is in positive size and in size zero (For , the characteristic polynomial is when , with for the unique matrix).
Proof
If , [L4] gives .
Suppose and choose from [L1]. Over , .
By [L2], . Since , multiplicativity also gives .
Using [L4] in step 2.1 gives , and step 1.1 supplies the remaining size.
Depends on
- For $A\in M_n(F)$, the characteristic polynomial is $\chi_A(x)=\det(xI_n-A)$ when $n\geq1$, with $\chi_A(x)=1$ for the unique $0\times0$ matrix
- Similar matrices: $B=P^{-1}AP$ for an invertible $P$
- For same-sized finite square matrices over a commutative ring, $\det(AB)=\det(A)\det(B)$
- For a field, the ring-matrix operations, invertibility and similarity agree exactly with the established field-matrix interface
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 49 results over 12 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.1 (standard reference, not scraped)