theorem Th15: :: VECTSP11:15

for K being Field
for L being Scalar of K
for V1 being finite-dimensional VectSp of K
for b1, b19 being OrdBasis of V1
for f being linear-transformation of V1,V1 holds
( ( f is with_eigenvalues & L is eigenvalue of f ) iff Det (AutEqMt ((f + ((- L) * (id V1))),b1,b19)) = 0. K )