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 a finite-dimensional vector space, a decomposable wedge is nonzero exactly when its vectors are linearly independent

Statement

Let $V$ be a finite-dimensional vector space over $F$ . For $v_{1}, \dots, v_{k} \in V$ ,

$v_{1} \land \dots \land v_{k} \neq 0 ⟺ v_{1}, \dots, v_{k} are linearly independent .$

Facts & Assumptions

Given: A finite-dimensional vector space $V$ over a field $F$ and a finite list $v_{1}, \dots, v_{k}$ .

[L1]

A list is dependent exactly when one entry is a linear combination of the others (Linear independence: a finite list $v : n \to V$ is independent when $\sum_{i < n} λ_{i} v_{i} = 0_{V}$ forces every $λ_{i} = 0_{F}$ , and a subset $S \subseteq V$ is independent when every injective finite list into $S$ is independent).

[L2]

The increasing-index wedges of a basis form a basis of $Λ^{k} V$ (Increasing-index wedges of a basis form a basis of $Λ^{k} V$ ).

[L3]

In a finite-dimensional vector space, every linearly independent subset is contained in a basis, with no choice principle needed (If $\dim_{F} V = n$ and $U$ is a linear subspace of $V$ , then $U$ is finite-dimensional, $\dim_{F} U \leq n$ , and $\dim_{F} U = n$ if and only if $U = V$ ).

Proof

technique · direct

1.1L1algebra

If $v_{1}, \dots, v_{k}$ are dependent, choose by [L1] an entry $v_{j} = \sum_{i \neq j} c_{i} v_{i}$ . Expanding the wedge by the multilinearity of the wedge map gives $v_{1} \land \dots \land v_{k} = \sum_{i \neq j} c_{i} (v_{1} \land \dots \land v_{i} \land \dots \land v_{k})$ with $v_{i}$ in the $j$ th slot, and every summand has the repeated entry $v_{i}$ , so alternation kills it; hence the wedge is zero.

1.2L2L3

If $v_{1}, \dots, v_{k}$ are independent, [L3] places the subset ${v_{1}, \dots, v_{k}}$ inside a basis of $V$ ; ordering the remaining basis vectors after $v_{1}, \dots, v_{k}$ gives a basis $(v_{1}, \dots, v_{k}, u_{k + 1}, \dots, u_{n})$ of $V$ . Then $v_{1} \land \dots \land v_{k}$ is the basis wedge attached to the first $k$ indices, so by [L2] it is a basis vector and in particular nonzero.

2.1step 1.1step 1.2∎

Steps 1.1 and 1.2 prove the two directions of the equivalence.

Depends on

Used by

Dependency tree · two levels

30 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)