PropositionStatement: 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.

Exterior multiplication and interior product satisfy the graded anticommutation identity

Statement

For vectors $v, w$ in a finite-dimensional real inner product space $V$ and every $α \in Λ^{k} V$ ,

$ι_{v} (w \land α) + w \land ι_{v} (α) = ⟨ v, w ⟩ α .$

Facts & Assumptions

Given: Vectors $v, w \in V$ and an element $α \in Λ^{k} V$ .

[L1]

The interior product is the adjoint of exterior multiplication: $⟨ ι_{v} α, β ⟩ = ⟨ α, v \land β ⟩$ (Interior product on the exterior algebra).

[L2]

On a decomposable wedge, $ι_{v} (v_{1} \land \dots \land v_{k}) = \sum_{r = 1}^{k} (- 1)^{r - 1} ⟨ v, v_{r} ⟩ v_{1} \land \dots \land \hat{v_{r}} \land \dots \land v_{k}$ (Interior product is the adjoint of exterior multiplication by a vector).

[L3]

The wedge product is bilinear, associative, and satisfies $v \land w = - w \land v$ for vectors (Exterior multiplication is well defined, graded, associative, unital, and graded-commutative).

Proof

technique · direct

1.1

For a decomposable $α = v_{1} \land \dots \land v_{k}$ , apply [L2] to $w \land α = w \land v_{1} \land \dots \land v_{k}$ : the $r = 0$ term is $⟨ v, w ⟩ v_{1} \land \dots \land v_{k}$ , and the terms $r \geq 1$ contribute $- \sum_{r = 1}^{k} (- 1)^{r - 1} ⟨ v, v_{r} ⟩ w \land v_{1} \land \dots \land \hat{v_{r}} \land \dots \land v_{k}$ , because the omission of $v_{r}$ leaves $w$ in position $r + 1$ , which costs the sign $(- 1)^{r}$ .

L2algebra

2.1

Using [L3] to move the leading $w$ and [L2] once more identifies the sum over $r \geq 1$ with $- w \land ι_{v} (α)$ , so $ι_{v} (w \land α) = ⟨ v, w ⟩ α - w \land ι_{v} (α)$ .

step 1.1L2L3

3.1

Both sides of the claimed identity are linear in $α$ (the wedge is bilinear by [L3] and $ι_{v}$ is linear by [L1]), so equality extends from decomposables to all of $Λ^{k} V$ .

step 2.1L1L3∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

10 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

Albert Chern, Geometric Fluid Dynamics notes, Interior Products (standard reference, not scraped)