Alphabeta MathHow 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 and every commutative ring , the Leibniz determinant is column-multilinear, alternating and normalized.
Facts & Assumptions
Given: The Leibniz determinant of an matrix over a commutative ring.
Determinant is the finite signed sum over (For , the determinant over a commutative ring by the Leibniz formula, and for a real matrix).
Multilinear, alternating and normalized have the stated columnwise meanings (Column-multilinear, alternating, normalized and antisymmetric functions on square matrices over a commutative ring).
Sign is a homomorphism on (The sign is a homomorphism , surjective exactly when ).
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).
Composing a permutation on either side with a transposition reverses its inversion sign (Composing with a transposition reverses ).
Proof
With every column but column fixed, each Leibniz monomial contains exactly one entry from column . Distributing finite sums therefore proves additivity and scalar compatibility in that column, and was arbitrary.
Suppose columns are equal. Pair each with . Commutativity makes the paired monomials equal, while [L5] makes their signs opposite, so every pair sums to zero and the determinant vanishes.
At , every nonidentity permutation selects an off-diagonal zero, while the identity term is . Thus . This also covers and the zero ring, where the equality reads .
Depends on
- For $n\ge1$, the determinant over a commutative ring by the Leibniz formula, and $|\det A|$ for a real matrix
- Column-multilinear, alternating, normalized and antisymmetric functions on square matrices over a commutative ring
- Composing with a transposition reverses $(-1)^{\operatorname{inv}(\sigma)}$
- The sign is a homomorphism $S_n\to\{+1,-1\}$, surjective exactly when $n\ge 2$
- Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule
Used by
- A square matrix with a zero column or two equal columns has determinant zero Corollary
- An invertible square matrix over a commutative ring has unit determinant Corollary
- If A is invertible over a commutative ring, then det(A⁻¹)=det(A)⁻¹ Corollary
- The determinant is alternating and multilinear in the rows as well as in the columns Corollary
- FALSE: det(A+B)=det(A)+det(B) for all same-sized square matrices False statement
- The determinant is the unique normalized alternating multilinear function on the columns Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 88 results over 15 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
- S. New, MATH 146 Linear Algebra 1 Lecture Notes, Theorems 4.19–4.22 (standard reference, not scraped)
- P. Massot, Structures algébriques fondamentales, Definition 6.4.1 (standard reference, not scraped)