ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck 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.

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∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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

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