:: deftheorem Def4 defines nilpotent MATRIXJ2:def 4 :
for K being doubleLoopStr
for V being non empty ModuleStr over K
for f being Function of V,V holds
( f is nilpotent iff ex n being Nat st
for v being Vector of V holds (f |^ n) . v = 0. V );