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.

✓ 7 results · all verified · 0 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 7 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Matrices and Change of Basis: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-11Open item page →

A matrix represents a map $F^{2} \to F^{3}$ by its images of the standard basis vectors

Example

Over a field $F$ , define

$T : F^{2} \to F^{3}, T (x, y) = (x + 2 y, 3 x - y, x + y) .$

In the standard ordered bases,

$[T] = (\begin{array}{cc} 1 & 2 \\ 3 & - 1 \\ 1 & 1 \end{array}),$

whose columns are the coordinate columns of $T (1, 0)$ and $T (0, 1)$ .

Facts & Assumptions

Given: The displayed linear map and the standard ordered bases of $F^{2}$ and $F^{3}$ .

[L1]

The $j$ -th column of a linear map's matrix is the coordinate column of the image of the $j$ -th domain basis vector (Coordinate columns $[v]_{B}$ and matrices $[T]_{B}^{C}$ of linear maps relative to ordered bases).

Verification

technique · direct

1.1

One has $T (1, 0) = (1, 3, 1)$ and $T (0, 1) = (2, - 1, 1)$ , so [L1] gives the two displayed columns and hence the displayed $3$ by $2$ matrix.

givenL1

2.1

Multiplication by a general coordinate column gives $(\begin{array}{cc} 1 & 2 \\ 3 & - 1 \\ 1 & 1 \end{array}) (\begin{array}{c} x \\ y \end{array}) = (\begin{array}{c} x + 2 y \\ 3 x - y \\ x + y \end{array}) = [T (x, y)]$ , independently verifying that the matrix represents $T$ .

step 1.1L1∎

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-11Open item page →

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∎

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-11Open item page →

The quarter-turn $(x, y) \mapsto (- y, x)$ on $R^{2}$ has matrix $(\begin{array}{cc} 0 & - 1 \\ 1 & 0 \end{array})$ and square $- I_{2}$

Example

The linear map $Q : R^{2} \to R^{2}$ given by $Q (x, y) = (- y, x)$ is a quarter-turn. In the standard basis,

$[Q] = (\begin{array}{cc} 0 & - 1 \\ 1 & 0 \end{array}), [Q]^{2} = - I_{2} .$

Thus $Q^{2} (x, y) = (- x, - y)$ is the half-turn.

Facts & Assumptions

Given: The real vector space $R^{2}$ with its standard ordered basis and the displayed map $Q$ .

[L1]

The columns of a linear map's matrix are the coordinate columns of its basis-vector images (Coordinate columns $[v]_{B}$ and matrices $[T]_{B}^{C}$ of linear maps relative to ordered bases).

[L2]

The matrix of a composite is the product of the matrices ( $[S \circ T]_{B}^{D} = [S]_{C}^{D} [T]_{B}^{C}$ ).

Verification

technique · direct

1.1

Since $Q (1, 0) = (0, 1)$ and $Q (0, 1) = (- 1, 0)$ , [L1] gives $[Q] = (\begin{array}{cc} 0 & - 1 \\ 1 & 0 \end{array})$ . Multiplying this matrix by itself gives $(\begin{array}{cc} - 1 & 0 \\ 0 & - 1 \end{array}) = - I_{2}$ .

givenL1

2.1

By [L2], the matrix square is $[Q^{2}]$ , and direct substitution gives $Q^{2} (x, y) = Q (- y, x) = (- x, - y)$ , the half-turn.

step 1.1L1L2∎

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-11Open item page →

Two explicit $2$ by $2$ matrices do not commute

Example

In $M_{2} (F)$ , let

$A = E_{01} = (\begin{array}{cc} 0 & 1 \\ 0 & 0 \end{array}), B = E_{10} = (\begin{array}{cc} 0 & 0 \\ 1 & 0 \end{array}) .$

Then $A B \neq B A$ .

Facts & Assumptions

Given: A field $F$ and the displayed matrix units in $M_{2} (F)$ .

[L1]

Matrix units satisfy $E_{i j} E_{k ℓ} = δ_{j k} E_{i ℓ}$ ( $E_{i j} E_{k ℓ} = δ_{j k} E_{i ℓ}$ ).

Verification

technique · direct

1.1

By [L1], $A B = E_{00} = (\begin{array}{cc} 1 & 0 \\ 0 & 0 \end{array})$ while $B A = E_{11} = (\begin{array}{cc} 0 & 0 \\ 0 & 1 \end{array})$ .

givenL1

2.1

The products differ at entry $(0, 0)$ , since $1 \neq 0$ in a field, so $A$ and $B$ do not commute.

step 1.1L1∎

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-11Open item page →

A nonzero square-zero matrix is not similar to any diagonal matrix

Example

For every field $F$ , the matrix

$N = E_{01} = (\begin{array}{cc} 0 & 1 \\ 0 & 0 \end{array}) \in M_{2} (F)$

is nonzero and satisfies $N^{2} = 0$ , but it is not similar to any diagonal matrix.

Facts & Assumptions

Given: A field $F$ and the displayed matrix $N$ .

[L1]

Matrix units satisfy $E_{i j} E_{k ℓ} = δ_{j k} E_{i ℓ}$ ( $E_{i j} E_{k ℓ} = δ_{j k} E_{i ℓ}$ ).

[L2]

Similarity has the form $N = P^{- 1} D P$ with $P$ invertible, and every nonzero scalar in a field has an inverse (Similar matrices: $B = P^{- 1} A P$ for an invertible $P$ , Field).

Verification

technique · contradiction

1.1

By [L1], $N^{2} = E_{01} E_{01} = 0$ , while the $(0, 1)$ -entry of $N$ is $1$ , so $N \neq 0$ . Suppose, for contradiction, that $N = P^{- 1} D P$ as in [L2], with $D$ diagonal. Then $0 = N^{2} = P^{- 1} D^{2} P$ , so $D^{2} = 0$ .

assume-contraL1L2

2.1

Every diagonal entry $d$ of $D$ satisfies $d^{2} = 0$ . If $d \neq 0$ , the inverse from [L2] gives $d = 0$ , a contradiction; hence $D = 0$ , and then $N = P^{- 1} 0 P = 0$ , contradicting step 1.1. Thus $N$ is not similar to a diagonal matrix.

step 1.1L1L2discharge-contradiction∎

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-11Open item page →

Changing both domain and codomain bases of a map $F^{2} \to F^{3}$ uses both sides of the formula

Example

Let $T : F^{2} \to F^{3}$ be $T (x, y) = (x + 2 y, 3 x - y, x + y)$ . Use the standard bases $B, C$ and the new bases

$B^{'} = (e_{0} + e_{1}, e_{1}), C^{'} = (f_{0} + f_{2}, f_{1}, f_{2}) .$

Then

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

Facts & Assumptions

Given: The displayed map and four ordered bases.

[L1]

The two-sided formula is $[T]_{B^{'}}^{C^{'}} = P_{C^{'} \leftarrow C} [T]_{B}^{C} P_{B \leftarrow B^{'}}$ ( $[T]_{B^{'}}^{C^{'}} = P_{C^{'} \leftarrow C} [T]_{B}^{C} P_{B \leftarrow B^{'}}$ ).

Verification

technique · direct

1.1

Here $[T]_{B}^{C} = (\begin{array}{cc} 1 & 2 \\ 3 & - 1 \\ 1 & 1 \end{array})$ , $P_{B \leftarrow B^{'}} = (\begin{array}{cc} 1 & 0 \\ 1 & 1 \end{array})$ , and $P_{C^{'} \leftarrow C} = (\begin{array}{ccc} 1 & 0 & 0 \\ 0 & 1 & 0 \\ - 1 & 0 & 1 \end{array})$ . Multiplying in the order of [L1] gives $(\begin{array}{cc} 3 & 2 \\ 2 & - 1 \\ - 1 & - 1 \end{array})$ .

givenL1

2.1

Independently, $T (e_{0} + e_{1}) = (3, 2, 2) = 3 (f_{0} + f_{2}) + 2 f_{1} - f_{2}$ and $T (e_{1}) = (2, - 1, 1) = 2 (f_{0} + f_{2}) - f_{1} - f_{2}$ , producing the same two coordinate columns.

step 1.1L1∎

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-11Open item page →

A $2$ by $3$ matrix and a $3$ by $2$ matrix give square products of different sizes but equal traces

Example

Over any field $F$ , let

$A = (\begin{array}{ccc} 1 & 2 & 0 \\ 0 & 1 & 3 \end{array}), B = (\begin{array}{cc} 1 & 0 \\ 2 & 1 \\ 0 & 1 \end{array}) .$

The product $A B$ is $2$ by $2$ , the product $B A$ is $3$ by $3$ , and their traces are equal.

Facts & Assumptions

Given: The displayed rectangular matrices over a field $F$ .

[L1]

For conformable rectangular matrices, $tr (A B) = tr (B A)$ (For $A \in M_{m \times n} (F)$ and $B \in M_{n \times m} (F)$ , $tr (A B) = tr (B A)$ ).

Verification

technique · direct

1.1

Direct multiplication gives $A B = (\begin{array}{cc} 5 & 2 \\ 2 & 4 \end{array})$ and $B A = (\begin{array}{ccc} 1 & 2 & 0 \\ 2 & 5 & 3 \\ 0 & 1 & 3 \end{array})$ .

givenL1

2.1

Hence $tr (A B) = 5 + 4 = 9$ and $tr (B A) = 1 + 5 + 3 = 9$ as elements of $F$ , verifying [L1] for products of different square sizes.

step 1.1L1∎

Matrices and Change of Basis: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

A matrix represents a map F2→F3F2→F3 by its images of the standard basis vectors

Example

Facts & Assumptions

Verification

The same operator has two different matrices in two ordered bases

Example

Facts & Assumptions

Verification

The quarter-turn (x,y)↦(−y,x)(x,y)↦(−y,x) on R2R2 has matrix (0−110)(01​−10​) and square −I2−I2​

Example

Facts & Assumptions

Verification

Two explicit 22 by 22 matrices do not commute

Example

Facts & Assumptions

Verification

A nonzero square-zero matrix is not similar to any diagonal matrix

Example

Facts & Assumptions

Verification

Changing both domain and codomain bases of a map F2→F3F2→F3 uses both sides of the formula

Example

Facts & Assumptions

Verification

A 22 by 33 matrix and a 33 by 22 matrix give square products of different sizes but equal traces

Example

Facts & Assumptions

Verification

Sources

A matrix represents a map $F^{2} \to F^{3}$ by its images of the standard basis vectors

The quarter-turn $(x, y) \mapsto (- y, x)$ on $R^{2}$ has matrix $(\begin{array}{cc} 0 & - 1 \\ 1 & 0 \end{array})$ and square $- I_{2}$

Two explicit $2$ by $2$ matrices do not commute

Changing both domain and codomain bases of a map $F^{2} \to F^{3}$ uses both sides of the formula

A $2$ by $3$ matrix and a $3$ by $2$ matrix give square products of different sizes but equal traces