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
- Determinant is additive in one selected column but not under simultaneous whole-matrix addition Example
- FALSE: det(A+B)=det(A)+det(B) for all same-sized square matrices False statement
- For A∈ Mₙ(R) and columns u,v over a commutative ring, det(A+uv^T)=det(A)+v^Tadj(A)u Lemma
- Cramer's rule over a commutative ring: every solution satisfies det(A)xⱼ=det(Aⱼ(b)), and a unit determinant gives the unique quotient formula Theorem
- Increasing-index wedges of a basis form a basis of ΛᵏV Theorem
- Laplace expansion computes the determinant along every row and every column over a commutative ring Theorem
- On a positive-dimensional space, det(T) is the unique scalar by which T scales every alternating top-degree form Theorem
- The Binet-Cauchy formula Theorem
- The determinant is the unique normalized alternating multilinear function on the columns Theorem
Dependency tree · two levels
25 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
- 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)