theorem :: MATRIXJ2:8

for n being Nat
for K being Field
for L being Element of K st L <> 0. K holds
ex M being Matrix of n,K st
( (Jordan_block (L,n)) ~ = M & ( for i, j being Nat st [i,j] in Indices M holds
( ( i > j implies M * (i,j) = 0. K ) & ( i <= j implies M * (i,j) = - ((power K) . ((- (L ")),((j -' i) + 1))) ) ) ) )