let n be Nat; :: thesis: for K being Field
for L being Element of K holds Det (Jordan_block (L,n)) = (power K) . (L,n)
let K be Field; :: thesis: for L being Element of K holds Det (Jordan_block (L,n)) = (power K) . (L,n)
let L be Element of K; :: thesis: Det (Jordan_block (L,n)) = (power K) . (L,n)
thus Det (Jordan_block (L,n)) = the multF of K $$ (diagonal_of_Matrix (Jordan_block (L,n))) by MATRIX13:7
.= Product (n |-> L) by Th1
.= (power K) . (L,n) by MATRIXJ1:5 ; :: thesis: verum