for n being Nat
for K being Field
for L being Element of K holds
( Jordan_block (L,n) is invertible iff ( n = 0 or L <> 0. K ) )