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.
A square matrix has an unpivoted unit-lower LU factorisation exactly when all leading principal minors are nonzero
Statement
Let be a field, let , and let . For , let be the determinant of the leading principal submatrix .
Then has a normalised LU factorisation whose upper factor has nonzero diagonal if and only if
In particular, the condition forces , so is invertible.
Facts & Assumptions
Given: A field , a natural number , and a matrix .
A normalised LU factorisation is with unit lower triangular and upper triangular (A normalised LU factorisation has a unit lower-triangular L and an upper-triangular U).
An invertible leading block gives the block LU factorisation through its Schur complement (An invertible leading block yields block LU through its Schur complement).
The determinant of a triangular matrix is the product of its diagonal entries (The determinant of a triangular matrix is the product of its diagonal entries).
Determinants are multiplicative (For same-sized finite square matrices over a commutative ring, ).
Proof
Suppose as in [L1] and that the diagonal of is nonzero. For each , the leading block also factors as , where is unit lower triangular and is upper triangular with diagonal . By [L3] and [L4],
For the converse, use induction on . When , the condition is , and is already a normalised LU factorisation with nonzero diagonal.
Assume and the converse for size . Write Then . Set . For each , apply [L2] to the leading block of : its determinant is , where is the leading block of . Hence By the induction hypothesis, has a normalised LU factorisation with nonzero diagonal.
Step 1.3 and [L2] give which is a normalised LU factorisation of . Its upper diagonal is followed by the diagonal of , so it is nonzero.
Step 1.1 proves the forward implication, and steps 1.2-2.1 prove the reverse implication for every . The final sentence is the case .
Depends on
- A normalised LU factorisation has a unit lower-triangular L and an upper-triangular U
- An invertible leading block yields block LU through its Schur complement
- The determinant of a triangular matrix is the product of its diagonal entries
- For same-sized finite square matrices over a commutative ring, $\det(AB)=\det(A)\det(B)$
Used by
Dependency tree · two levels
14 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
- Tobin A. Driscoll and Richard J. Braun, Fundamentals of Numerical Computation, Section 2.6 (standard reference, not scraped)
- David Bindel, CS 4220: Numerical Analysis, Blocked LU and Cholesky (standard reference, not scraped)