refactor(linear_algebra/eigenspace): cleanup proof (#7337)
At some point we changed the proof of `exists_eigenvalue` so that it used the fact that any endomorphism of a vector space is integral. This means we don't actually need to pick a nonzero vector at any point, but the proof had been left in a hybrid state, which I've now cleaned up.
In a later PR I'll generalise this proof so it proves Schur's lemma.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
