for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K holds
( ( f is with_eigenvalues & L is eigenvalue of f ) iff not ker (f + ((- L) * (id V1))) is trivial )