for n being Nat
for K being Field
for L being Element of K holds diagonal_of_Matrix (Jordan_block (L,n)) = n |-> L