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.
Statement
Let be linear. If are ordered bases of and are ordered bases of , then
Facts & Assumptions
Given: The linear map and four ordered bases in the Statement.
is the matrix of the identity map converting -coordinates to -coordinates (The change-of-basis matrix ).
Proof
Regard from to as the composite of the identity on from to , then from to , then the identity on from to .
Applying [L2] twice, with the matrix of the last-applied map on the left, gives
The right factor is square of size , the middle factor has shape , and the left factor is square of size , so the product is defined and has the asserted shape, proving the formula.
Depends on
- The change-of-basis matrix $P_{\mathcal C\leftarrow\mathcal B}=[\operatorname{id}_V]_{\mathcal B}^{\mathcal C}$
- $[v]_{\mathcal C}=P_{\mathcal C\leftarrow\mathcal B}[v]_{\mathcal B}$ and $P_{\mathcal B\leftarrow\mathcal C}=P_{\mathcal C\leftarrow\mathcal B}^{-1}$
- $[S\circ T]_{\mathcal B}^{\mathcal D}=[S]_{\mathcal C}^{\mathcal D}[T]_{\mathcal B}^{\mathcal C}$
Used by
- The adjugate of an operator on a positive-dimensional finite-dimensional vector space, defined by the adjugate matrix in any basis Definition
- Changing both domain and codomain bases of a map F²→ F³ uses both sides of the formula Example
- One operator has matrices diag(2,3) and beginpmatrix2&01&3 endpmatrix in two bases, both with determinant 6 Example
- The same operator has two different matrices in two ordered bases Example
- Similarity is an equivalence relation, and two matrices represent the same endomorphism in two bases exactly when they are similar Theorem
Dependency tree · two levels
9 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., §3D, results 3.81 and 3.84 (standard reference, not scraped)
- S. Schiavone, MIT 18.700 Day 9, change of basis (standard reference, not scraped)