I can now say exactly what I don't like about the theorem statement: That the definition of the eigenvalue notation was not well-scoped. This made it much harde

I can now say exactly what I don't like about the theorem statement: That the definition of the eigenvalue notation was not well-scoped. This made it much harder for me to understand what is going on, and has nothing to do with the actual semantic meaning of eigenvalues. Caring about proper scoping is also something mathematicians usually do not, making everything more complicated than it has to be in the process.