for K being Field
for L being Element of K
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for J being FinSequence_of_Jordan_block of L,K
for M being Matrix of len b1, len b1,K st M = block_diagonal (J,(0. K)) holds
( Mx2Tran (M,b1,b1) is nilpotent iff ( len b1 = 0 or L = 0. K ) )