:: deftheorem Def2 defines eigenvalue VECTSP11:def 2 :
for R being non empty doubleLoopStr
for V being non empty ModuleStr over R
for f being Function of V,V st f is with_eigenvalues holds
for b₄ being Element of R holds
( b₄ is eigenvalue of f iff ex v being Vector of V st
( v <> 0. V & f . v = b₄ * v ) );