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.

Increasing-index wedges of a basis form a basis of $Λ^{k} V$

Statement

Let $V$ have the ordered basis $(e_{1}, \dots, e_{n})$ over $F$ and let $0 \leq k \leq n$ . For each $k$ -element subset $I = {i_{1} < \dots < i_{k}} \subseteq {1, \dots, n}$ write

$e_{I} : = e_{i_{1}} \land \dots \land e_{i_{k}} .$

Then the family $(e_{I})_{I}$ indexed by the $k$ -element subsets of ${1, \dots, n}$ is a basis of $Λ^{k} V$ .

Facts & Assumptions

Given: A vector space $V$ with ordered basis $(e_{1}, \dots, e_{n})$ and a degree $0 \leq k \leq n$ .

[L1]

The exterior power is $Λ^{k} V = V^{\otimes k} / W_{k}$ with the wedge equal to the universal multilinear map composed with the quotient projection (The $k$ th exterior power as the tensor-power quotient by repeated-vector relations).

[L2]

The pure tensors $e_{i_{1}} \otimes \dots \otimes e_{i_{k}}$ over all $k$ -tuples form a basis of $V^{\otimes k}$ (The elementary tensors of two bases form the product basis of the tensor product).

[L3]

Alternating $k$ -linear maps factor uniquely through $Λ^{k} V$ (Exterior powers represent alternating multilinear maps and are unique up to unique isomorphism).

[L4]

A basis is a linearly independent spanning set (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis).

[L5]

For $k \geq 1$ , the matrix determinant is alternating and multilinear in the columns, with $\det (I_{k}) = 1$ (The Leibniz determinant is column-multilinear, alternating and normalized over every commutative ring).

Proof

technique · direct

1.1L1

If $k = 0$ , then [L1] gives $Λ^{0} V = F$ , and the unique $0$ -element subset of ${1, \dots, n}$ is $\emptyset$ , with $e_{\emptyset} : = 1_{F}$ a basis of $F$ . So only the case $k \geq 1$ remains.

1.2L1L2

Assume $k \geq 1$ . By [L2], every element of $V^{\otimes k}$ is a linear combination of the pure tensors over all $k$ -tuples; passing to the quotient of [L1], every element of $Λ^{k} V$ is a linear combination of the wedges $e_{i_{1}} \land \dots \land e_{i_{k}}$ over all $k$ -tuples.

1.3L1algebra

Still assuming $k \geq 1$ , a wedge with a repeated index is zero by [L1], and a wedge with distinct indices equals the increasing-index wedge up to a sign: transposing two adjacent wedge entries multiplies the wedge by $- 1$ , because by [L1] the alternating relation gives $0 = (\dots v + w \dots v + w \dots) = (\dots v \dots w \dots) + (\dots w \dots v \dots)$ .

1.4L3L5

For each $k$ -subset $J = {j_{1} < \dots < j_{k}}$ define $φ_{J} : V^{k} \to F$ by $φ_{J} (v_{1}, \dots, v_{k}) : = \det M$ , where $M$ is the $k \times k$ matrix whose $r$ th column is the list of the $j_{1}, \dots, j_{k}$ coordinates of $v_{r}$ ; by [L5], $φ_{J}$ is $k$ -linear and alternating, so [L3] induces a unique linear map ${\overline{φ}}_{J} : Λ^{k} V \to F$ with ${\overline{φ}}_{J} (v_{1} \land \dots \land v_{k}) = φ_{J} (v_{1}, \dots, v_{k})$ .

2.1step 1.2step 1.3L4

If $k \geq 1$ , then steps 1.2 and 1.3 give that the increasing wedges $e_{I}$ span $Λ^{k} V$ .

2.2L5step 1.4

If $k \geq 1$ , then for subsets $I, J$ , the matrix for $φ_{J}$ at $(e_{i_{1}}, \dots, e_{i_{k}})$ is the identity when $I = J$ and has a zero row when $I \neq J$ , so [L5] and step 1.4 give ${\overline{φ}}_{J} (e_{I}) = 1$ for $I = J$ and $0$ for $I \neq J$ .

3.1step 1.4step 2.2L4

If $k \geq 1$ and $\sum_{I} c_{I} e_{I} = 0$ , applying ${\overline{φ}}_{J}$ of step 1.4 gives $c_{J} = 0$ for every $J$ by step 2.2, so the increasing wedges are linearly independent in the sense of [L4].

4.1step 1.1step 2.1step 3.1L4∎

Step 1.1 handles $k = 0$ , while steps 2.1 and 3.1 show that for $k \geq 1$ the increasing wedges are a spanning independent set. Therefore in every case the family $(e_{I})_{I}$ is a basis of $Λ^{k} V$ .

Depends on

Used by

Dependency tree · two levels

38 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

Keith Conrad, Exterior Powers (standard reference, not scraped)

Increasing-index wedges of a basis form a basis of ΛkVΛkV