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 determinant of a triangular matrix is the product of its diagonal entries
Statement
If is upper or lower triangular over a commutative ring, with , then
Facts & Assumptions
Given: A triangular matrix over a commutative ring.
Upper triangular means for , while lower triangular means for (Upper triangular, lower triangular and diagonal square matrices over a commutative ring).
Determinant is the sum of the signed products (For , the determinant over a commutative ring by the Leibniz formula, and for a real matrix).
The identity permutation has sign (Inversions, inversion number, the sign , and even and odd permutations).
Proof
For an upper triangular matrix, a nonzero Leibniz term requires for every . A permutation with these inequalities is the identity: starting at and proceeding upward, bijectivity forces . Thus every nonidentity term contains a zero entry.
The identity term has sign and equals , so it is the whole determinant.
For a lower triangular matrix the same argument uses and proceeds downward, again forcing the identity. The argument includes and makes no cancellation assumption, so zero divisors and the zero ring cause no exception.
Depends on
- Upper triangular, lower triangular and diagonal square matrices over a commutative ring
- For $n\ge1$, the determinant over a commutative ring by the Leibniz formula, and $|\det A|$ for a real matrix
- Inversions, inversion number, the sign $\operatorname{sgn}(\sigma)=(-1)^{\operatorname{inv}(\sigma)}$, and even and odd permutations
Used by
- In positive dimension the determinant of an operator is computed from a representing matrix by row reduction, tracking swaps and row scalings Corollary
- The index of a full-rank subgroup of ℤⁿ is the absolute determinant of a generating matrix Corollary
- A sparse 4×4 determinant is 30 by both cofactor expansion and row reduction Example
- Brownian finite-dimensional density Example
- Row operations track determinant correctly for a singular triangular matrix over ℤ/6 Example
- The Lebesgue measure of the image of the unit cube under an explicit linear map of the plane and of three-space Example
- A coordinate scaling and a coordinate transposition send the unit cube to a set of measure equal to the absolute value of the determinant Lemma
- A shear sends the unit cube to a set of Lebesgue measure one Lemma
- For symmetric M=beginpmatrixA&BB^T&C endpmatrix with A invertible, a block-unitriangular congruence gives A⊕(C-B^TA⁻¹B) and factors det M Lemma
- The real Jacobian determinant of a complex-linear automorphism is the squared modulus of its complex determinant Lemma
- A finite square real matrix is invertible if and only if its determinant is nonzero Theorem
- A Gram determinant is nonnegative and is positive exactly when the vector list is linearly independent Theorem
- A linear map T of ℝⁿ sends Lebesgue measurable sets to Lebesgue measurable sets, with λₙ(T[E])=|det T| λₙ(E) when T is invertible and T[E] Lebesgue null when it is not Theorem
- A matrix admits a Cholesky factorisation with positive diagonal exactly when it is Hermitian positive definite, and that factor is unique Theorem
- A square matrix has an unpivoted unit-lower LU factorisation exactly when all leading principal minors are nonzero Theorem
- An endomorphism is diagonalisable if and only if its characteristic polynomial splits and every eigenvalue's geometric multiplicity equals its algebraic multiplicity Theorem
- For real symmetric matrices, positive leading principal minors are equivalent to positive Cholesky pivots 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
Dependency tree · two levels
15 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, Ch. 4 (standard reference, not scraped)
- D. Margalit and J. Rabinoff, Interactive Linear Algebra, §4.1 (standard reference, not scraped)