ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-11

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.

The same operator has two different matrices in two ordered bases

Example

Let $T : F^{2} \to F^{2}$ be $T (x, y) = (x, 2 y)$ . In the standard ordered basis $E = (e_{0}, e_{1})$ ,

$[T]_{E}^{E} = (\begin{array}{cc} 1 & 0 \\ 0 & 2 \end{array}) .$

For $B = (e_{0} + e_{1}, e_{1})$ , the same operator has

$[T]_{B}^{B} = (\begin{array}{cc} 1 & 0 \\ 1 & 2 \end{array}) .$

Facts & Assumptions

Given: The displayed operator and ordered bases.

[L1]

A matrix of an operator records the coordinate columns of its basis-vector images, and basis change acts by the two-sided formula (Coordinate columns $[v]_{B}$ and matrices $[T]_{B}^{C}$ of linear maps relative to ordered bases, $[T]_{B^{'}}^{C^{'}} = P_{C^{'} \leftarrow C} [T]_{B}^{C} P_{B \leftarrow B^{'}}$ ).

Verification

technique · direct

1.1

The standard images are $T (e_{0}) = e_{0}$ and $T (e_{1}) = 2 e_{1}$ . The transition matrices are $P_{E \leftarrow B} = (\begin{array}{cc} 1 & 0 \\ 1 & 1 \end{array})$ and $P_{B \leftarrow E} = (\begin{array}{cc} 1 & 0 \\ - 1 & 1 \end{array})$ , whose products in either order are $I_{2}$ .

givenL1

2.1

Directly, $T (e_{0} + e_{1}) = e_{0} + 2 e_{1} = (e_{0} + e_{1}) + e_{1}$ and $T (e_{1}) = 2 e_{1}$ , giving the columns $(1, 1)$ and $(0, 2)$ . Equivalently, $P_{B \leftarrow E} [T]_{E}^{E} P_{E \leftarrow B} = (\begin{array}{cc} 1 & 0 \\ 1 & 2 \end{array})$ .

step 1.1L1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

11 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., Example 3.83 (standard reference, not scraped)