theorem Th31: :: MATRIXJ2:31

for K being algebraic-closed Field
for V being non trivial finite-dimensional VectSp of K
for F being linear-transformation of V,V ex J being non-empty FinSequence_of_Jordan_block of K ex b1 being OrdBasis of V st
( AutMt (F,b1,b1) = block_diagonal (J,(0. K)) & ( for L being Scalar of K holds
( L is eigenvalue of F iff ex i being Nat st
( i in dom J & J . i = Jordan_block (L,(len (J . i))) ) ) ) )