:: deftheorem Def5 defines degree_of_nilpotent MATRIXJ2:def 5 :
for K being doubleLoopStr
for V being non empty ModuleStr over K
for f being nilpotent Function of V,V
for b₄ being Nat holds
( b₄ = degree_of_nilpotent f iff ( f |^ b₄ = ZeroMap (V,V) & ( for k being Nat st f |^ k = ZeroMap (V,V) holds
b₄ <= k ) ) );