Product_of_Triangular_Matrices
Provedlinear-algebramatrixproductproofwikitriangular
Let be upper triangular matrices of order . Let . Then the diagonal elements of are given by That is, the diagonal elements of are those of the factor matrices multiplied together. The matrix is itself upper triangular. The same applies if both and are lower triangular matrices.
Preamble
import Mathlib.Data.Matrix.Basic
Formal statement
theorem Product_of_Triangular_Matrices {R : Type _} [CommRing R] {n : ℕ} (A B : Matrix (Fin n) (Fin n) R) (hA : ∀ i j : Fin n, j < i → A i j = 0) (hB : ∀ i j : Fin n, j < i → B i j = 0) : ∀ i j : Fin n, j < i → (A * B) i j = 0 := by sorrySource