Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13
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.

In dual bases, the matrix of T∗ is the transpose of the matrix of T

Statement

Let T:V→W be linear between finite-dimensional spaces, with ordered bases V=(v1,…,vn) and W=(w1,…,wm). In the dual bases,

[T∗]W∗V∗=([T]VW)T.

Facts & Assumptions

Given: The displayed map, bases, and their dual bases.

[L2]

The dual families of the finite bases are bases of the dual spaces (The dual family of a finite basis is a basis of the dual space, with the same dimension).

[L3]

The jth column of a representing matrix is the coordinate column of the image of the jth basis vector (Coordinate columns [v]B and matrices [T]BC of linear maps relative to ordered bases).

[L4]

The transpose of an m×n matrix has (j,i) entry equal to the original (i,j) entry (The transpose AT of a matrix).

Proof

technique · entrywise comparison
1.1

Write [T]VW=(aij), so [L3] gives T(vj)=∑i=1maijwi and therefore wi∗(T(vj))=aij.

L2L3algebra
2.1

The (j,i) entry of [T∗]W∗V∗ is the coefficient of vj∗ in the expansion of T∗(wi∗)∈V∗ along the dual basis V∗. Since every ϕ∈V∗ satisfies ϕ=∑jϕ(vj)vj∗, that coefficient is T∗(wi∗)(vj), which by [L1] equals wi∗(T(vj))=aij.

step 1.1L1L2L3
3.1

By [L4], step 2.1 says exactly that the n×m matrix of T∗ is the transpose of the m×n matrix of T. The calculation also covers m=0 or n=0, where the matrices are empty rectangles.

step 2.1L4∎

Depends on

Used by

Dependency tree · two levels

12 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