for n being Nat
for K being Field
for M being lower_triangular Matrix of n,K holds Det M = the multF of K $$ (diagonal_of_Matrix M)