Matrix_is_Row_Equivalent_to_Echelon_Matrix

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

linear-algebramatrixproofwikirow-echelon

Let $\mathbf A = \sqbrk a_{m n}$ be a matrix of order $m \times n$ over a field $F$ . Then $A$ is row equivalent to a reduced echelon matrix of order $m \times n$ .

Preamble

import Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Formal statement

theorem Matrix_is_Row_Equivalent_to_Echelon_Matrix {F : Type _} [Field F] {m n : ℕ} (A : Matrix (Fin m) (Fin n) F) : ∃ (B : Matrix (Fin m) (Fin n) F) (P : Matrix (Fin m) (Fin m) F), IsUnit P ∧ B = P * A := by sorry

Source

https://proofwiki.org/wiki/Matrix_is_Row_Equivalent_to_Reduced_Echelon_Matrix

View graph