LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11

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.

Every alternating multilinear $F$ satisfies $F (A) = F (I) \sum_{σ \in S_{n}} sgn (σ) \prod_{i} a_{σ (i), i}$

Statement

Let $n \geq 1$ , let $R$ be a commutative ring, and let $F : M_{n} (R) \to R$ be alternating and column-multilinear. Then for $A = (a_{r i})$ , $F (A) = F (I_{n}) \sum_{σ \in S_{n}} sgn (σ) \prod_{i < n} a_{σ (i), i} .$

Facts & Assumptions

Given: A matrix $A = (a_{r i}) \in M_{n} (R)$ and an alternating column-multilinear function $F : M_{n} (R) \to R$ .

[L1]

Column multilinearity expands $F$ in each column (Column-multilinear, alternating, normalized and antisymmetric functions on square matrices over a commutative ring).

[L2]

Alternating multilinear functions are antisymmetric under swaps (Every alternating multilinear matrix function is antisymmetric under a column swap).

[L3]

The sign of a permutation is $(- 1)^{inv (σ)}$ (Inversions, inversion number, the sign $sgn (σ) = (- 1)^{inv (σ)}$ , and even and odd permutations).

[L4]

Sign is a homomorphism on $S_{n}$ (The sign is a homomorphism $S_{n} \to {+ 1, - 1}$ , surjective exactly when $n \geq 2$ ).

[L5]

Finite sums and products over finite index sets are defined in commutative monoids (A finite sum in a commutative monoid indexed by an arbitrary finite set, The product $g_{0} g_{1} \dots g_{n - 1}$ of a finite list in a monoid, by recursion, with the empty product ( $n = 0$ ) equal to the identity).

[L6]

Every finite permutation is a product of transpositions (Every finite permutation is a product of transpositions, so the transpositions generate $S_{n}$ ).

[L7]

Every transposition factorisation of a permutation has parity prescribed by its inversion sign (Every transposition factorisation of $σ$ has parity $(- 1)^{inv (σ)}$ ).

Proof

technique · direct

1.1L1L5algebra

For $r < n$ , let $e_{r}$ be the column with entry $1$ in row $r$ and $0$ elsewhere. Since column $i$ is $\sum_{r < n} a_{r i} e_{r}$ , repeated multilinearity expands $F (A)$ as the finite sum over tuples $(r_{i})_{i < n}$ of $(\prod_{i < n} a_{r_{i} i}) F (e_{r_{0}}, \dots, e_{r_{n - 1}})$ .

2.1step 1.1L1

If a tuple repeats a row index, its $F$ -value is zero by alternation. The surviving tuples use every element of $n$ once, so they are precisely the permutations $r_{i} = σ (i)$ .

3.1step 2.1L2L3L4L6L7algebra∎

Factor $σ$ into transpositions. Repeated antisymmetry changes $F (I_{n})$ by one minus sign per transposition. Each transposition has sign $- 1$ , so [L4] identifies the product of these signs with $sgn (σ)$ ; equivalently [L3] and [L7] identify it with the factorisation-independent inversion parity. Substitution into step 2.1 gives the formula.

Every alternating multilinear $F$ satisfies $F (A) = F (I) \sum_{σ \in S_{n}} sgn (σ) \prod_{i} a_{σ (i), i}$

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

Every alternating multilinear FF satisfies F(A)=F(I)∑σ∈Snsgn⁡(σ)∏iaσ(i),iF(A)=F(I)∑σ∈Sn​​sgn(σ)∏i​aσ(i),i​

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

Every alternating multilinear $F$ satisfies $F (A) = F (I) \sum_{σ \in S_{n}} sgn (σ) \prod_{i} a_{σ (i), i}$