Row echelon forms

This file defines the row echelon form of matrices and the leading entries of their rows.

Main definitions

• Matrix.IsRowEchelon expresses that A is in row echelon form: an entry of a lower row vanishes whenever a higher row is zero at every column strictly to its left.
• Matrix.IsLeadingEntry: c : n is the leading position of row i of A.
• Matrix.IsReducedRowEchelon additionally requires each leading entry to be 1 and the entries above it to vanish.

Tags

matrix, echelon form

def Matrix.IsRowEchelon {m : Type u_1} {n : Type u_2} {R : Type v} [Zero R] [LT m] [LT n] (A : Matrix m n R) : Prop

A is in row echelon form: for rows i₁ < i₂, if the higher row i₁ is zero at every column strictly left of j₂, then the lower row i₂ is zero at j₂.

Equations

• A.IsRowEchelon = ∀ ⦃i₁ i₂ : m⦄, i₁ < i₂ → ∀ ⦃j₂ : n⦄, (∀ j₁ < j₂, A i₁ j₁ = 0) → A i₂ j₂ = 0

theorem Matrix.IsRowEchelon.row_eq_zero_of_lt {m : Type u_1} {n : Type u_2} {R : Type v} {A : Matrix m n R} [Zero R] [LT m] [LT n] {i₁ i₂ : m} (he : A.IsRowEchelon) (hlt : i₁ < i₂) (h0 : A i₁ = 0) : A i₂ = 0

In an echelon matrix, rows below a zero row are zero.

Leading entries

def Matrix.IsLeadingEntry {m : Type u_1} {n : Type u_2} {R : Type v} [Zero R] [LT n] (A : Matrix m n R) (i : m) (c : n) : Prop

c is the leading position of row i.

Equations

• A.IsLeadingEntry i c = ((∀ j < c, A i j = 0) ∧ A i c ≠ 0)

theorem Matrix.IsLeadingEntry.row_ne_zero {m : Type u_1} {n : Type u_2} {R : Type v} {A : Matrix m n R} [Zero R] [LT n] {i : m} {c : n} (hc : A.IsLeadingEntry i c) : A i ≠ 0

theorem Matrix.row_ne_zero_iff_exists_isLeadingEntry {m : Type u_1} {n : Type u_2} {R : Type v} {A : Matrix m n R} [Zero R] [LT n] [WellFoundedLT n] {i : m} : A i ≠ 0 ↔ ∃ (c : n), A.IsLeadingEntry i c

theorem Matrix.IsLeadingEntry.unique {m : Type u_1} {n : Type u_2} {R : Type v} {A : Matrix m n R} [Zero R] [LinearOrder n] {i : m} {c₁ c₂ : n} (h₁ : A.IsLeadingEntry i c₁) (h₂ : A.IsLeadingEntry i c₂) : c₁ = c₂

If column indices have a linear order, then there's at most one leading position per row.

@[instance_reducible]

instance Matrix.instDecidableIsLeadingEntryOfDecidableEqOfFintypeOfDecidableLT {m : Type u_1} {n : Type u_2} {R : Type v} [Zero R] [DecidableEq R] [Fintype n] [LT n] [DecidableLT n] (A : Matrix m n R) (i : m) (c : n) : Decidable (A.IsLeadingEntry i c)

Equations

• A.instDecidableIsLeadingEntryOfDecidableEqOfFintypeOfDecidableLT i c = decidable_of_iff ((∀ j < c, A i j = 0) ∧ A i c ≠ 0) ⋯

Reduced row echelon form

structure Matrix.IsReducedRowEchelon {m : Type u_1} {n : Type u_2} {R : Type v} [Zero R] [LT m] [LT n] [One R] (A : Matrix m n R) : Prop

A is in reduced row echelon form: it is in row echelon form, each leading entry is 1, and entries above a leading entry vanish (entries below one vanish by isRowEchelon).

• isRowEchelon : A.IsRowEchelon
• eq_one ⦃i : m⦄ ⦃c : n⦄ (hA : A.IsLeadingEntry i c) : A i c = 1
• eq_zero ⦃i₁ i₂ : m⦄ ⦃c : n⦄ (hlt : i₁ < i₂) (hA : A.IsLeadingEntry i₂ c) : A i₁ c = 0

theorem Matrix.IsReducedRowEchelon.eq_zero_of_ne_of_isLeadingEntry {m : Type u_1} {n : Type u_2} {R : Type v} {A : Matrix m n R} [Zero R] [LinearOrder m] [LT n] [One R] {i₁ i₂ : m} {c : n} (hA : A.IsReducedRowEchelon) (hne : i₁ ≠ i₂) (hlead : A.IsLeadingEntry i₂ c) : A i₁ c = 0

If the row indices have a linear order, then every entry in a pivot column vanishes except for the pivot.

Properties of row echelon forms

theorem Matrix.IsRowEchelon.isUpperTriangular {m : Type u_1} {R : Type v} {A : Matrix m m R} [LT m] [WellFoundedLT m] [Zero R] (hA : A.IsRowEchelon) : A.IsUpperTriangular

theorem Matrix.IsRowEchelon.det_eq {m : Type u_1} {R : Type v} {A : Matrix m m R} [DecidableEq m] [Fintype m] [LinearOrder m] [CommRing R] (hA : A.IsRowEchelon) : A.det = ∏ i : m, A i i