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