:: deftheorem Def1 defines Jordan_block MATRIXJ2:def 1 :
for K being Field
for L being Element of K
for n being Nat
for b₄ being Matrix of K holds
( b₄ = Jordan_block (L,n) iff ( len b₄ = n & width b₄ = n & ( for i, j being Nat st [i,j] in Indices b₄ holds
( ( i = j implies b₄ * (i,j) = L ) & ( i + 1 = j implies b₄ * (i,j) = 1_ K ) & ( i <> j & i + 1 <> j implies b₄ * (i,j) = 0. K ) ) ) ) );