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.

The Gram formula gives a well-defined positive-definite inner product on exterior powers, and $∥ v_{1} \land \dots \land v_{k} ∥^{2}$ is the Gram determinant

Statement

Let $V$ be a finite-dimensional real inner product space of dimension $n$ , and let $0 \leq k \leq n$ . The formula

$⟨ v_{1} \land \dots \land v_{k}, w_{1} \land \dots \land w_{k} ⟩ = \det (⟨ v_{i}, w_{j} ⟩)_{i, j \leq k}$

defines a well-defined inner product on $Λ^{k} V$ in the sense of Real and complex inner product spaces, with the inner product linear in the first argument. In particular, for every list $(v_{1}, \dots, v_{k})$ ,

$∥ v_{1} \land \dots \land v_{k} ∥^{2} = \det G (v_{1}, \dots, v_{k}),$

the Gram determinant of The Gram matrix $G (v_{0}, \dots, v_{r - 1}) = (⟨ v_{i}, v_{j} ⟩)_{i, j < r}$ and Gram determinant, with empty value $1$ , which vanishes exactly when the list is dependent.

Facts & Assumptions

Given: A finite-dimensional real inner product space $V$ of dimension $n$ , a degree $0 \leq k \leq n$ , and lists of length $k$ in $V$ .

[L1]

The intended pairing is the displayed determinant formula, with descent through the quotient in each slot (The Gram inner product on $Λ^{k} V$ ).

[L2]

The Gram matrix is $G (v_{1}, \dots, v_{k}) = (⟨ v_{i}, v_{j} ⟩)_{i, j}$ , with empty determinant $1$ (The Gram matrix $G (v_{0}, \dots, v_{r - 1}) = (⟨ v_{i}, v_{j} ⟩)_{i, j < r}$ and Gram determinant, with empty value $1$ ).

[L3]

The Gram determinant is nonnegative, and positive exactly for independent lists (A Gram determinant is nonnegative and is positive exactly when the vector list is linearly independent).

[L4]

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

[L5]

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

[L6]

A finite-dimensional inner product space has an orthonormal basis (Every finite-dimensional real or complex inner product space has an orthonormal basis).

[L7]

The determinant is unchanged by transposition: $\det (M^{T}) = \det M$ (For every square matrix over a commutative ring, $\det (A^{T}) = \det (A)$ ).

Proof

technique · direct

1.1L1L5

For a fixed list $(w_{1}, \dots, w_{k})$ , the assignment $(v_{1}, \dots, v_{k}) \mapsto \det (⟨ v_{i}, w_{j} ⟩)$ is $k$ -linear and alternating in the $v$ 's (determinant multilinear in rows, zero on a repeated row), so by [L5] it descends to a unique linear functional on $Λ^{k} V$ ; symmetrically in the second slot. This is the well-defined bilinear pairing of [L1].

1.2L1L2

By [L1] and [L2], the pure-wedge norm square is $∥ v_{1} \land \dots \land v_{k} ∥^{2} = \det G (v_{1}, \dots, v_{k})$ .

1.3L2L7

Symmetry: $⟨ β, α ⟩ = \det (⟨ w_{j}, v_{i} ⟩) = \det ((⟨ v_{i}, w_{j} ⟩)^{T}) = ⟨ α, β ⟩$ by [L7].

2.1step 1.2L2L4L6

Choose an orthonormal basis $(e_{1}, \dots, e_{n})$ by [L6]; by [L4] the wedges $e_{I}$ form a basis of $Λ^{k} V$ , and by step 1.2 the pairing satisfies $⟨ e_{I}, e_{J} ⟩ = \det$ of the identity submatrix, which is $1$ when $I = J$ and $0$ otherwise.

2.2step 1.2L3

The norm-square formula of step 1.2 is the claimed Gram-determinant identity, and by [L3] that determinant is nonnegative and vanishes exactly for dependent lists, matching the independence criterion of In a finite-dimensional vector space, a decomposable wedge is nonzero exactly when its vectors are linearly independent.

3.1step 1.1step 1.3step 2.1algebra

Expanding $α = \sum_{I} c_{I} e_{I}$ in the basis of step 2.1 gives $⟨ α, α ⟩ = \sum_{I} c_{I}^{2} \geq 0$ , with equality exactly when every $c_{I} = 0$ , i.e. $α = 0$ ; with steps 1.1 and 1.3 this is a positive-definite inner product.

4.1step 1.1step 1.2step 2.2step 3.1∎

Steps 1.1, 2.2 and 3.1 prove well-definedness, the Gram-determinant formula, and positive definiteness.

Depends on

Used by

Interior product on the exterior algebra Definition
The oriented unit volume form Definition
Oriented area and volume are recovered from wedges and Gram determinants Example
FALSE: an orientation determines an inner product False statement
Interior product is the adjoint of exterior multiplication by a vector Theorem
The Hodge star exists uniquely and is given by the complementary-basis formula in an oriented orthonormal basis Theorem

Cited to discharge well-definedness by The Gram inner product on ΛᵏV.

Dependency tree · two levels

32 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

Reyer Sjamaar, Manifolds and Differential Forms, §8.1 (standard reference, not scraped)

The Gram formula gives a well-defined positive-definite inner product on exterior powers, and ∥v1∧⋯∧vk∥2∥v1​∧⋯∧vk​∥2 is the Gram determinant