:: deftheorem defines lower_triangular MATRIX_1:def 9 :
for n being Nat
for K being non empty ZeroStr
for M being Matrix of n,K holds
( M is lower_triangular iff for i, j being Nat st [i,j] in Indices M & i < j holds
M * (i,j) = 0. K );