Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck 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≥1, and let B=(b0,…,bn−1) be an ordered basis. If ω:Vn→F is alternating and linear in each argument, then

ω(v0,…,vn−1)=ω(b0,…,bn−1)det⁡MB(v0,…,vn−1),

where MB(v0,…,vn−1) has the B-coordinate column of vj as column j. Thus ω is determined by its value on B.

Facts & Assumptions

Given: V,F,n,B,ω, and v0,…,vn−1 as in the statement.

[F2]

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

[L1]

If G:Mn(F)→F is alternating and column-multilinear, then G(A)=G(In)det⁡(A) (Every alternating multilinear F satisfies F(A)=F(I)∑σ∈Snsgn⁡(σ)∏iaσ(i),i).

Proof

technique · direct
1.1

For A∈Mn(F), let wj be the unique vector whose B-coordinate column is column j of A, and define G(A):=ω(w0,…,wn−1). This is well defined, alternating, and column-multilinear.

F1F2given
2.1

The rigidity lemma gives G(A)=G(In)det⁡(A).

step 1.1L1
3.1

For A=MB(v0,…,vn−1), one has G(A)=ω(v0,…,vn−1) and G(In)=ω(b0,…,bn−1). Substitution in step 2.1 proves the formula and the final determination claim.

step 2.1F2∎

Depends on

Used by

Dependency tree · two levels

27 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