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

The Leibniz determinant is column-multilinear, alternating and normalized over every commutative ring

Statement

For $n \geq 1$ and every commutative ring $R$ , the Leibniz determinant $\det : M_{n} (R) \to R$ is column-multilinear, alternating and normalized.

Facts & Assumptions

Given: The Leibniz determinant of an $n \times n$ matrix over a commutative ring.

[L1]

Determinant is the finite signed sum over $S_{n}$ (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix).

[L2]

Multilinear, alternating and normalized have the stated columnwise meanings (Column-multilinear, alternating, normalized and antisymmetric functions on square matrices over a commutative ring).

[L3]

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

[L4]

Finite sums may be distributed and reindexed by bijections (Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule).

[L5]

Composing a permutation on either side with a transposition reverses its inversion sign (Composing with a transposition reverses $(- 1)^{inv (σ)}$ ).

Proof

technique · direct

1.1L1L2L4algebra

With every column but column $q$ fixed, each Leibniz monomial contains exactly one entry from column $q$ . Distributing finite sums therefore proves additivity and scalar compatibility in that column, and $q$ was arbitrary.

2.1step 1.1L3L4L5algebra

Suppose columns $p, q$ are equal. Pair each $σ$ with $σ \circ (p q)$ . Commutativity makes the paired monomials equal, while [L5] makes their signs opposite, so every pair sums to zero and the determinant vanishes.

3.1step 2.1L1L2algebra∎

At $I_{n}$ , every nonidentity permutation selects an off-diagonal zero, while the identity term is $1$ . Thus $\det (I_{n}) = 1$ . This also covers $n = 1$ and the zero ring, where the equality reads $0 = 0$ .

The Leibniz determinant is column-multilinear, alternating and normalized over every commutative ring

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources