Ah, that's very interesting. It looks very close to the fact that if a subfield of C has finite dimension over Q, then it consists of algebraic numbers.
It's a shame that you deleted the proof, I think it would have been a valuable addition (especially with a view towards formalizing Galois theory inside set.mm). -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/dbbd8f54-a8c5-4d7a-8b75-af1158830d47%40googlegroups.com.
