Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-08-29
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 basis-wedge coordinates, the matrix of ΛkT is the signed matrix of k-minors

Statement

Let V,W be finite-dimensional with ordered bases (e1,…,en) and (f1,…,fm), let T:V→W be linear with matrix A=(aij), so T(ej)=∑iaijfi, and let 1≤k≤min⁡(n,m). In the wedge bases (eI) and (fJ) of Increasing-index wedges of a basis form a basis of ΛkV, the matrix of ΛkT has entries

[ΛkT]J,I=det⁡AJ,I,

where AJ,I is the k×k submatrix of A with rows J={j1<⋯<jk} and columns I={i1<⋯<ik}.

Facts & Assumptions

Given: Ordered bases, a linear map T with matrix A, and k-subsets I,J.

[L1]

The induced map is ΛkT(eI)=T(ei1)∧⋯∧T(eik) (The induced map ΛkT on exterior powers).

[L2]

The jth column of A is the coordinate column of T(ej), i.e. T(ej)=∑iaijfi (Coordinate columns [v]B and matrices [T]BC of linear maps relative to ordered bases).

[L3]

The wedge families (eI) and (fJ) are bases of the exterior powers (Increasing-index wedges of a basis form a basis of ΛkV).

[L4]

The matrix determinant is the Leibniz sum det⁡B=∑σsgn⁡(σ)∏rbσ(r),r (For n≥1, the determinant over a commutative ring by the Leibniz formula, and ∣det⁡A∣ for a real matrix).

Proof

technique · direct
1.1L1

By [L1], ΛkT(eI)=T(ei1)∧⋯∧T(eik).

1.2L2

By [L2], each factor expands as T(eir)=∑mam,irfm.

1.3L3

By [L3], the wedges fJ form a basis of ΛkW.

2.1step 1.1step 1.2L4algebra

Expanding step 1.1 with step 1.2 and collecting the coefficient of fJ=fj1∧⋯∧fjk: only tuples with distinct indices survive (a repeated index makes the wedge zero), and reordering the tuple into increasing order multiplies by the permutation sign, so the coefficient is ∑σ∈Sksgn⁡(σ) ajσ(1),i1⋯ajσ(k),ik, which is det⁡AJ,I by [L4].

3.1step 1.3step 2.1L2∎

By step 1.3 and [L2], the coefficients computed in step 2.1 are exactly the entries of the matrix of ΛkT in the wedge bases.

Depends on

Used by

Dependency tree · two levels

23 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