theorem Matrix.IsUpperTriangular.imp {n : Type u_1} {R : Type u_2} [Zero R] [LT n] {A : Matrix n n R} (hA : A.IsUpperTriangular) ⦃i j : n⦄ (hij : j < i) : A i j = 0

theorem Matrix.mul_apply_diag_eq_mul_of_isUpperTriangular {n : Type u_1} {R : Type u_2} [NonUnitalNonAssocSemiring R] [LinearOrder n] [Fintype n] (A B : Matrix n n R) (hA : A.IsUpperTriangular) (hB : B.IsUpperTriangular) (i : n) : (A * B) i i = A i i * B i i