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.1

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].

L1L5

1.2

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})$ .

L1L2

1.3

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

L2L7

2.1

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.

step 1.2L2L4L6

2.2

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.

step 1.2L3

3.1

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.

step 1.1step 1.3step 2.1algebra

4.1

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

step 1.1step 1.2step 2.2step 3.1∎

Depends on

Used by

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