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 $Λ^{k} T$ is the signed matrix of $k$ -minors

Statement

Let $V, W$ be finite-dimensional with ordered bases $(e_{1}, \dots, e_{n})$ and $(f_{1}, \dots, f_{m})$ , let $T : V \to W$ be linear with matrix $A = (a_{i j})$ , so $T (e_{j}) = \sum_{i} a_{i j} f_{i}$ , and let $1 \leq k \leq \min (n, m)$ . In the wedge bases $(e_{I})$ and $(f_{J})$ of Increasing-index wedges of a basis form a basis of $Λ^{k} V$ , the matrix of $Λ^{k} T$ has entries

$[Λ^{k} T]_{J, I} = \det A_{J, I},$

where $A_{J, I}$ is the $k \times k$ submatrix of $A$ with rows $J = {j_{1} < \dots < j_{k}}$ and columns $I = {i_{1} < \dots < i_{k}}$ .

Facts & Assumptions

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

[L1]

The induced map is $Λ^{k} T (e_{I}) = T (e_{i_{1}}) \land \dots \land T (e_{i_{k}})$ (The induced map $Λ^{k} T$ on exterior powers).

[L2]

The $j$ th column of $A$ is the coordinate column of $T (e_{j})$ , i.e. $T (e_{j}) = \sum_{i} a_{i j} f_{i}$ (Coordinate columns $[v]_{B}$ and matrices $[T]_{B}^{C}$ of linear maps relative to ordered bases).

[L3]

The wedge families $(e_{I})$ and $(f_{J})$ are bases of the exterior powers (Increasing-index wedges of a basis form a basis of $Λ^{k} V$ ).

[L4]

The matrix determinant is the Leibniz sum $\det B = \sum_{σ} sgn (σ) \prod_{r} b_{σ (r), r}$ (For $n \geq 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], $Λ^{k} T (e_{I}) = T (e_{i_{1}}) \land \dots \land T (e_{i_{k}})$ .

1.2L2

By [L2], each factor expands as $T (e_{i_{r}}) = \sum_{m} a_{m, i_{r}} f_{m}$ .

1.3L3

By [L3], the wedges $f_{J}$ form a basis of $Λ^{k} W$ .

2.1step 1.1step 1.2L4algebra

Expanding step 1.1 with step 1.2 and collecting the coefficient of $f_{J} = f_{j_{1}} \land \dots \land f_{j_{k}}$ : 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 $\sum_{σ \in S_{k}} sgn (σ) a_{j_{σ (1)}, i_{1}} \dots a_{j_{σ (k)}, i_{k}}$ , which is $\det A_{J, 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 $Λ^{k} T$ in the wedge bases.

Depends on

Dependency tree · 2 levels

Sources

Keith Conrad, Exterior Powers

In basis-wedge coordinates, the matrix of ΛkTΛkT is the signed matrix of kk-minors