let n be Nat; :: thesis: for K being Field
for M being lower_triangular Matrix of n,K holds Det M = the multF of K $$ (diagonal_of_Matrix M)
let K be Field; :: thesis: for M being lower_triangular Matrix of n,K holds Det M = the multF of K $$ (diagonal_of_Matrix M)
let M be lower_triangular Matrix of n,K; :: thesis: Det M = the multF of K $$ (diagonal_of_Matrix M)
A1: Det M = Det (M @) by MATRIXR2:43;
M @ is upper_triangular Matrix of n,K by Th2;
hence Det M = the multF of K $$ (diagonal_of_Matrix (M @)) by A1, Th7
.= the multF of K $$ (diagonal_of_Matrix M) by Th3 ;
:: thesis: verum