Gaussian elimination and row echelon form

TheoremRow echelon form via a row permutation and a unit lower-triangular matrix#✓fully proved

Let \(K\) be a field and let \(A\) be a matrix over \(K\) whose rows and columns are indexed by finite linearly ordered sets. Then there are a permutation \(\sigma\) of the row indices and a square matrix \(L\) over \(K\) indexed by the row indices, lower triangular with every diagonal entry equal to \(1\), such that the matrix \(L A_\sigma\) is in row echelon form. Here \(A_\sigma\) is the matrix with entries \((A_\sigma)_{ic} = A_{\sigma(i) c}\), and a matrix \(B\) is in row echelon form when for all rows \(i_1 < i_2\) and every column \(c\), if \(B_{i_1 c'} = 0\) for every column \(c' < c\), then \(B_{i_2 c} = 0\).

theorem _root_.Matrix.exists_unitLowerTriangular_mul_submatrix_isRowEchelon
    {K m n : Type*} [Field K] [Fintype m] [LinearOrder m]
    [Finite n] [LinearOrder n] (A : Matrix m n K) :
    ∃ (L : Matrix m m K) (σ : Equiv.Perm m),
      L.IsLowerTriangular ∧ (∀ i, L.diag i = 1) ∧
        (L * A.submatrix σ id).IsRowEchelon

Used by 1

Used byGaussian elimination as a product of row operations

TheoremOne pivot step of Gaussian elimination#✓fully proved

Let \(K\) be a field and let \(A\) be a matrix over \(K\) whose rows are indexed by a finite linearly ordered set and whose columns are indexed by any set. Let \(r\) and \(i_0\) be row indices and \(j\) a column index with \(A_{i_0 j} \ne 0\), and let \(A'\) be the matrix obtained from \(A\) by exchanging rows \(r\) and \(i_0\). Then there is a square matrix \(P\) over \(K\) indexed by the row indices, lower triangular with every diagonal entry equal to \(1\), such that \((P A')_{i j} = 0\) for every row \(i > r\).

The row \(i_0\) may be any row with a nonzero entry in column \(j\); this is not magnitude-maximizing partial pivoting.

Proof: Use an entrywise unit lower-triangular matrix whose pivot column contains the elimination coefficients, then evaluate the matrix product as a finite sum (row operations of type 3, https://en.wikipedia.org/wiki/Gaussian_elimination).

theorem gauss_pivot_elim_step (A : Matrix m n K) (r : m) (j : n)
    (i₀ : m) (h : A i₀ j ≠ 0) :
    ∃ P : Matrix m m K, P.IsLowerTriangular ∧ (∀ i, P.diag i = 1) ∧
      ∀ i > r, (P * A.submatrix (Equiv.swap r i₀) id) i j = 0

Sources

• L. N. Trefethen and D. Bau, Numerical Linear Algebra, SIAM (1997), Lectures 20-21.

TheoremGaussian elimination as a product of row operations#✓fully proved

Let \(K\) be a field and let \(A\) be a matrix over \(K\) whose rows and columns are indexed by finite linearly ordered sets. Then there are a permutation \(\sigma\) of the row indices and a finite, possibly empty, list \(M_1, \dots, M_\ell\) of square matrices over \(K\) indexed by the row indices, each lower triangular with every diagonal entry equal to \(1\), such that the matrix \(M_1 M_2 \cdots M_\ell A_\sigma\) is in row echelon form. Here \(A_\sigma\) is the matrix with entries \((A_\sigma)_{ic} = A_{\sigma(i) c}\), the empty product is the identity matrix, and a matrix \(B\) is in row echelon form when for all rows \(i_1 < i_2\) and every column \(c\), if \(B_{i_1 c'} = 0\) for every column \(c' < c\), then \(B_{i_2 c} = 0\).

This records the factorization, not the intermediate matrices of an algorithm trace.

Proof: Induct on the columns after identifying the ordered index sets with initial segments of the natural numbers; a nonzero first column uses a row pivot and recurses on the lower-right block. Package the resulting single unit lower-triangular matrix as a one-element list (forward elimination to row echelon form, https://en.wikipedia.org/wiki/Gaussian_elimination).

theorem exists_gauss_elimination_opList (A : Matrix m n K) :
    ∃ (ops : List (Matrix m m K)) (σ : Equiv.Perm m),
      (∀ M ∈ ops, M.IsLowerTriangular ∧ ∀ i, M.diag i = 1) ∧
      (ops.prod * A.submatrix σ id).IsRowEchelon

Sources

• L. N. Trefethen and D. Bau, Numerical Linear Algebra, SIAM (1997), Lectures 20-21.

Uses 1

Proof usesRow echelon form via a row permutation and a unit lower-triangular matrix

TheoremPivot columns of a reduced row echelon matrix#✓fully proved

Let \(R\) be a type with elements \(0\) and \(1\), and let \(A\) be a matrix over \(R\) in reduced row echelon form whose rows are indexed by a linearly ordered set and whose columns are indexed by a set with a relation \(<\). Suppose that the leading entry of row \(i\) of \(A\) is in column \(c\), that is, \(A_{ic} \neq 0\) and \(A_{ij} = 0\) for every column \(j < c\). Then column \(c\) of \(A\) is the standard basis vector \(e_i\): \(A_{ic} = 1\) and \(A_{kc} = 0\) for every row \(k \neq i\).

theorem col_eq_single_of_isLeadingEntry
    [DecidableEq m] [LinearOrder m] [LT n]
    {A : Matrix m n R} (hA : A.IsReducedRowEchelon) {i : m} {c : n}
    (hc : A.IsLeadingEntry i c) : A.col c = Pi.single i 1

Used by 1

Used byUniqueness of the reduced row echelon form

TheoremOrder-preserving reindexing of columns preserves reduced row echelon form#✓fully proved

Let \(R\) be a type with elements \(0\) and \(1\), and let \(A\) be a matrix over \(R\) in reduced row echelon form whose rows are indexed by a linearly ordered set and whose columns are indexed by a linearly ordered set \(N\). Let \(e : O \to N\) be an order isomorphism from a linearly ordered set \(O\). Then the matrix \(B\) with columns indexed by \(O\) and entries \(B_{ik} = A_{i\,e(k)}\) is in reduced row echelon form.

theorem submatrix_orderIso
    [LinearOrder m] [LinearOrder n] {o : Type*} [LinearOrder o]
    {A : Matrix m n R} (hA : A.IsReducedRowEchelon)
    (e : o ≃o n) : (A.submatrix id e : Matrix m o R).IsReducedRowEchelon

Used by 1

Used byUniqueness of the reduced row echelon form

TheoremExistence of the reduced row echelon form#✓fully proved

Let \(K\) be a field, let \(m\) and \(n\) be finite linearly ordered sets, and let \(A\) be an \(m \times n\) matrix over \(K\). Then there are an \(m \times n\) matrix \(R\) over \(K\) in reduced row echelon form and an invertible \(m \times m\) matrix \(P\) over \(K\) with \(R = PA\). In other words, \(A\) is row-equivalent to a matrix in reduced row echelon form.

Proof: Choose pivot columns greedily (columns outside the span of the earlier ones), extend them to a basis of \(K^m\) whose order matches the order of the rows, and take \(R\) to be the coordinate matrix of the columns of \(A\) in that basis and \(P\) the matrix of the coordinate map.

theorem exists_isReducedRowEchelon_rowEquivalent
    (A : Matrix m n K) :
    ∃ (R : Matrix m n K) (P : Matrix m m K),
      R.IsReducedRowEchelon ∧ IsUnit P ∧ R = P * A

Sources

• G. Strang, Introduction to Linear Algebra, 6th ed., Wellesley-Cambridge Press (2023), Section 2.2.

TheoremUniqueness of the reduced row echelon form#✓fully proved

Let \(K\) be a field, let \(m\) and \(n\) be finite linearly ordered sets, and let \(R_1\) and \(R_2\) be \(m \times n\) matrices over \(K\) in reduced row echelon form. If \(R_2 = P R_1\) for some invertible \(m \times m\) matrix \(P\) over \(K\), then \(R_1 = R_2\). In other words, a row-equivalence class contains at most one matrix in reduced row echelon form.

Proof: Reindex the columns along the order isomorphism between \(\{0, \dots, |n| - 1\}\) and \(n\). For columns indexed by an initial segment of the natural numbers, induct on the number of columns: the matrices agree on all but the last column by induction, and that forces their last columns to agree.

theorem isReducedRowEchelon_unique_of_rowEquivalent
    (R₁ R₂ : Matrix m n K)
    (h₁ : R₁.IsReducedRowEchelon) (h₂ : R₂.IsReducedRowEchelon)
    (P : Matrix m m K) (hP : IsUnit P) (h : R₂ = P * R₁) :
    R₁ = R₂

Sources

• G. Strang, Introduction to Linear Algebra, 6th ed., Wellesley-Cambridge Press (2023), Section 2.2.

Uses 2

Proof usesPivot columns of a reduced row echelon matrix · Order-preserving reindexing of columns preserves reduced row echelon form

TheoremInvertible row operations preserve the null space#✓fully proved

Let \(K\) be a field, let \(m\) and \(n\) be finite sets, let \(A\) be an \(m \times n\) matrix over \(K\), and let \(P\) be an invertible \(m \times m\) matrix over \(K\). Then the linear maps \(x \mapsto PAx\) and \(x \mapsto Ax\) on \(K^n\) have the same kernel; that is, the homogeneous systems \(PAx = 0\) and \(Ax = 0\) have the same solutions.

Proof: For every \(x \in K^n\) we have \((PA)x = P(Ax)\), and multiplication by \(P\) is injective because \(P\) is invertible, so \((PA)x = 0\) if and only if \(Ax = 0\).

theorem ker_mulVecLin_mul_left_isUnit
    (P : Matrix m m K) (A : Matrix m n K) (hP : IsUnit P) :
    LinearMap.ker (Matrix.mulVecLin (P * A)) = LinearMap.ker (Matrix.mulVecLin A)

Sources

• G. Strang, Introduction to Linear Algebra, 6th ed., Wellesley-Cambridge Press (2023), Section 2.2.

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.