LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-01

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.

Wedge monomials in a dual basis form a basis

Statement

Let $e_{1}, \dots, e_{n}$ be a basis of $V$ , with dual basis $e^{1}, \dots, e^{n}$ . Then the wedges

e^{i_{1}} \land \dots \land e^{i_{k}} (1 \leq i_{1} < \dots < i_{k} \leq n)

form a basis of ${Alt}^{k} (V)$ .

Facts & Assumptions

Given: A basis $e_{1}, \dots, e_{n}$ of $V$ and its dual basis $e^{1}, \dots, e^{n}$ .

[F1]

The degree- $k$ part of the exterior algebra is ${Alt}^{k} (V)$ , with wedge product given by alternating tensor multiplication (The exterior algebra of covectors).

[L1]

Every covector expands in the dual basis, and $e^{i} (e_{j}) = δ_{j}^{i}$ (The dual family $(b^{*})_{b \in B}$ associated to a Hamel basis $B$ , defined by $b^{*} (c) = δ_{b c}$ ).

Proof

technique · direct

1.1

Let $ω \in {Alt}^{k} (V)$ . Expanding each input vector in the basis and using multilinearity shows that $ω$ is determined by its values on basis $k$ -tuples. Because $ω$ is alternating, every tuple with a repeated index vanishes and every tuple with distinct indices reduces, up to sign, to one with increasing indices. Thus $ω$ is a linear combination of the displayed wedges from [F1].

F1L1givenalgebra

2.1

Suppose $\sum_{I} c_{I} e^{I} = 0$ , where $I = (i_{1} < \dots < i_{k})$ and $e^{I} : = e^{i_{1}} \land \dots \land e^{i_{k}}$ . Evaluating at $(e_{j_{1}}, \dots, e_{j_{k}})$ with $j_{1} < \dots < j_{k}$ , [L1] gives $e^{I} (e_{j_{1}}, \dots, e_{j_{k}}) = 1$ when $I = (j_{1}, \dots, j_{k})$ and $0$ otherwise. Hence every $c_{I} = 0$ .

L1step 1.1algebra

3.1

Therefore the displayed wedges form a basis of ${Alt}^{k} (V)$ .

step 1.1step 2.1∎

Depends on

Used by

Dimension of the kth exterior power is binomial Corollary
Wedge products of the standard dual basis Example
Exterior-power duality pairing Proposition
Local coordinate expression for a differential form Proposition
Universal property of the finite-dimensional exterior power Theorem

Dependency tree · two levels

17 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

John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (standard reference, not scraped)