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 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
- Finite-candidate information design Algorithm
- 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
- The critical Riesz potential can diverge and be essentially unbounded Counterexample
- Standard subgroups of finite general linear groups Definition
- A sparse 4×4 determinant is 30 by both cofactor expansion and row reduction Example
- A unit-scale affine coupling has a triangular Jacobian Example
- Brownian finite-dimensional density Example
- Chebyshev extremals and the exact disk Fekete polynomial Example
- Dilation determines the Riesz-potential target exponent Example
- Regular and singular torus characters in GL₃(F_q) Example
- Row operations track determinant correctly for a singular triangular matrix over ℤ/6 Example
- The Coxeter complex of I₂(5): the circle triangulated by the ten chambers 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 determinant and Frobenius norm give a certified lower bound for small-block separation Lemma
- A Hermitian two-by-two pivot inertia is determined by determinant and trace signs Lemma
- A nonsingular principal minor of the symmetrized Cartan matrix of size the rank Lemma
- A shear sends the unit cube to a set of Lebesgue measure one Lemma
- A uniform positive eigenvalue floor controls log-determinant error Lemma
- An explicit root-separation bound for squarefree integer polynomials Lemma
- Bfgs trace and determinant identities give a matrix potential inequality Lemma
- Bounded compact data give an everywhere finite Newtonian potential Lemma
- Determinants and kernel quotients of the model Bergman metrics Lemma
- Fixed-memory L-Bfgs curvature and scale bounds imply uniform spectral bounds 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
- Gaussian integral for a positive-definite quadratic form Lemma
- Holomorphic Morse normalization and Gaussian contour Lemma
- Length-additive products of the standard intertwiners Lemma
- Near and far bounds for a Riesz potential Lemma
- Positively oriented bases of an oriented vector space are path-connected Lemma
- Powers of a Schur-stable matrix decay geometrically up to a polynomial factor Lemma
- Strict concavity of log determinant on positive-definite matrices Lemma
- The conditional Gaussian mixture is a nonnegative supermartingale Lemma
- The elliptical-potential bound for ridge design matrices Lemma
- The equal-coordinate rank-one principal series of GL₂ Lemma
- The log determinant is concave on positive-definite matrices Lemma
- The rank-one Hecke parameter for equal torus characters Lemma
- The real Jacobian determinant of a complex-linear automorphism is the squared modulus of its complex determinant Lemma
- The ridge information matrix is positive definite and invertible Lemma
…and 26 more results.
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)