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.
For every square matrix over a commutative ring,
Statement
For every , every commutative ring , and every ,
Facts & Assumptions
Given: A square matrix over a commutative ring.
Determinant is the Leibniz sum over permutations (For , the determinant over a commutative ring by the Leibniz formula, and for a real matrix).
Sign is a homomorphism into , so (The sign is a homomorphism , surjective exactly when ).
A finite sum may be reindexed by a bijection (Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule).
Proof
Substituting [L2] into [L1] gives .
Reindex the sum by and the product by . Commutativity and [L3] turn the expression into .
Depends on
- For $n\ge1$, the determinant over a commutative ring by the Leibniz formula, and $|\det A|$ for a real matrix
- Entrywise ring-matrix operations, rectangular matrix products, identity matrices and transpose
- 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
- Orthogonal and unitary operators form groups, and their determinants have modulus one Corollary
- The determinant is alternating and multilinear in the rows as well as in the columns Corollary
- Chart and partition independence of surface measure Lemma
- For a finite Galois extension, (αⱼ) is a base-field basis exactly when the matrix (σᵢαⱼ) is invertible Lemma
- The quaternion double cover generates the third homotopy group of SO(3) Lemma
- A Gram determinant is nonnegative and is positive exactly when the vector list is linearly independent Theorem
- Laplace expansion computes the determinant along every row and every column over a commutative ring Theorem
- Sylvester's criterion: a real symmetric n× n matrix with n≥1 is positive definite if and only if all leading principal minors are positive Theorem
- The Gram formula gives a well-defined positive-definite inner product on exterior powers, and ‖v₁∧⋯∧ vₖ‖² is the Gram determinant Theorem
Dependency tree · two levels
22 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, Theorem 4.23 (standard reference, not scraped)
- P. Massot, Structures algébriques fondamentales, Proposition 6.4.3 (standard reference, not scraped)