LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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.

An alternating top-degree form is determined by its value on one ordered basis

Statement

Let $V$ be an $n$ -dimensional vector space over a field $F$ , where $n \geq 1$ , and let $B = (b_{0}, \dots, b_{n - 1})$ be an ordered basis. If $ω : V^{n} \to F$ is alternating and linear in each argument, then

$ω (v_{0}, \dots, v_{n - 1}) = ω (b_{0}, \dots, b_{n - 1}) \det M_{B} (v_{0}, \dots, v_{n - 1}),$

where $M_{B} (v_{0}, \dots, v_{n - 1})$ has the $B$ -coordinate column of $v_{j}$ as column $j$ . Thus $ω$ is determined by its value on $B$ .

Facts & Assumptions

Given: $V, F, n, B, ω$ , and $v_{0}, \dots, v_{n - 1}$ as in the statement.

[F1]

An $n$ -dimensional vector space has an ordered basis of $n$ vectors (Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis).

[F2]

Every vector has a unique coordinate column in an ordered basis (Coordinate columns $[v]_{B}$ and matrices $[T]_{B}^{C}$ of linear maps relative to ordered bases).

[L1]

If $G : M_{n} (F) \to F$ is alternating and column-multilinear, then $G (A) = G (I_{n}) \det (A)$ (Every alternating multilinear $F$ satisfies $F (A) = F (I) \sum_{σ \in S_{n}} sgn (σ) \prod_{i} a_{σ (i), i}$ ).

Proof

technique · direct

1.1

For $A \in M_{n} (F)$ , let $w_{j}$ be the unique vector whose $B$ -coordinate column is column $j$ of $A$ , and define $G (A) : = ω (w_{0}, \dots, w_{n - 1})$ . This is well defined, alternating, and column-multilinear.

F1F2given

2.1

The rigidity lemma gives $G (A) = G (I_{n}) \det (A)$ .

step 1.1L1

3.1

For $A = M_{B} (v_{0}, \dots, v_{n - 1})$ , one has $G (A) = ω (v_{0}, \dots, v_{n - 1})$ and $G (I_{n}) = ω (b_{0}, \dots, b_{n - 1})$ . Substitution in step 2.1 proves the formula and the final determination claim.

step 2.1F2∎

Depends on

Used by

On a positive-dimensional space, det(T) is the unique scalar by which T scales every alternating top-degree form Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 78 results over 20 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Sheldon Axler, Linear Algebra Done Right, 4th ed. (standard reference, not scraped)