TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passaudited 2026-08-30

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.

When unpivoted elimination runs to completion, the elimination multipliers are the entries of the normalised LU factors

Statement

Let $n \geq 1$ , let $F$ be a field, and let $A \in M_{n} (F)$ . Assume unpivoted Gaussian elimination reaches an upper-triangular matrix without encountering a zero pivot. Let $m_{i k}$ be the multiplier used to eliminate entry $(i, k)$ , so the $k$ -th elimination matrix is

$E_{k} : = I - \sum_{i > k} m_{i k} e_{i} e_{k}^{T} .$ If $U : = E_{n - 2} \dots E_{0} A$ is the final upper-triangular matrix, with this product understood as the empty product and $U = A$ when $n = 1$ , then $A = L U,$

where $L$ is unit lower triangular and its strict lower entry in position $(i, k)$ is exactly $m_{i k}$ .

Facts & Assumptions

Given: An integer $n \geq 1$ , a field $F$ , a matrix $A \in M_{n} (F)$ , unpivoted Gaussian elimination with no zero pivot, the elimination matrices $E_{k}$ , and the final upper-triangular matrix $U = E_{n - 2} \dots E_{0} A$ , where $U = A$ when $n = 1$ .

[L1]

A normalised LU factorisation is $A = L U$ with $L$ unit lower triangular and $U$ upper triangular (A normalised LU factorisation has a unit lower-triangular L and an upper-triangular U).

[L2]

An invertible leading block yields block LU through the Schur complement (An invertible leading block yields block LU through its Schur complement).

[L3]

Matrix multiplication uses the usual product convention (Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes).

Proof

technique · induction on the elimination stages

1.1

At stage $k$ , the matrix $E_{k}$ is unit lower triangular and differs from $I$ only in column $k$ below the diagonal. Its inverse is $E_{k}^{- 1} = I + \sum_{i > k} m_{i k} e_{i} e_{k}^{T}$ , because all cross terms vanish: $e_{i} e_{k}^{T} e_{j} e_{k}^{T} = 0$ for $i, j > k$ . Thus $E_{k}^{- 1}$ is unit lower triangular with strict lower entries exactly the multipliers from column $k$ .

givenL3algebra

2.1

Since $U = E_{n - 2} \dots E_{0} A$ , one has $A = E_{0}^{- 1} \dots E_{n - 2}^{- 1} U$ . The product of unit lower triangular matrices is unit lower triangular, and the first time a strict lower entry in column $k$ appears is in $E_{k}^{- 1}$ , so later factors do not change that column above the already-created zeros. Hence the strict lower entries of $L : = E_{0}^{- 1} \dots E_{n - 2}^{- 1}$ are exactly the stored multipliers $m_{i k}$ .

step 1.1L3induction

3.1

The matrix $U$ is upper triangular by construction, so step 2.1 is a normalised LU factorisation in the sense of [L1]. This is the scalar-entry form of the same elimination mechanism that [L2] packages blockwise. Equivalently, the row operations of elimination store their multipliers in $L$ and leave the final reduced matrix as $U$ .

step 2.1L1L2

4.1

Steps 2.1 and 3.1 prove the claim.

step 2.1step 3.1discharge-induction∎

Depends on

Used by

Every real or complex square matrix admits a PLU factorisation, and the first failed pivot marks the singular boundary Theorem

Dependency tree · two levels

9 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

David Bindel, CS 4220: Numerical Analysis, Blocked LU and Cholesky (standard reference, not scraped)
Tobin A. Driscoll and Richard J. Braun, Fundamentals of Numerical Computation, Section 2.6 (standard reference, not scraped)