I still stand by my opening statement. Now, after the discussion here I understand what the theorem statement is saying. That's a lot of work I had to do to und

I still stand by my opening statement. Now, after the discussion here I understand what the theorem statement is saying. That's a lot of work I had to do to understand the theorem statement, and it would have been unnecessary, had the theorem been stated "syntactically" correctly. Now why wasn't the theorem stated syntactically correct? If we had to state it in a mechanised theorem prover like Isabelle then we would extract the definition of the eigenvalues from the statement into a separate definition, like: For a hermitian n x n matrix H, let lambda_1(A), ..., lambda_n(A) be the eigenvalues of H. But of course, here we assume an order of the eigenvalues, and we don't really want that, because it is immaterial to what follows. So we rather have to write it like that: Definition: For a matrix H, let L(H) be the set of its eigenvalues. Theorem: If H is a n x n Hermitian matrix, then |L(H)| = n. But, of course, this is not true, as |L(H)| < n is a possibility. So you would have to account for that somehow as well in your definition / notation. So it is probably better to go back instead again, and explain the notation as follows: Notation: For a Hermitian n x n matrix H, let lambda_1(H), ..., lambda_n(H) be its eigenvalues (in an arbitrary order). Theorem: What Tao said. The notation could still not be written in Isabelle like that, but at least it has proper scoping now.