:: deftheorem defines with_eigenvalues VECTSP11:def 1 :
for R being non empty doubleLoopStr
for V being non empty ModuleStr over R
for IT being Function of V,V holds
( IT is with_eigenvalues iff ex v being Vector of V ex a being Scalar of R st
( v <> 0. V & IT . v = a * v ) );