Square_Matrix_is_Row_Equivalent_to_Triangular_Matrix
Provedlinear-algebramatrixproofwikitriangular
Let be a square matrix of order over a commutative ring . Then can be converted to an upper or lower triangular matrix by elementary row operations.
Preamble
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Formal statement
theorem Square_Matrix_is_Row_Equivalent_to_Triangular_Matrix {R : Type _} [CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) : ∃ B : Matrix (Fin n) (Fin n) R, (∀ i j : Fin n, j < i → B i j = 0) ∧ A.det = B.det := by sorrySource