選択公理を認めると、複素数体には巨大な自己同型群が存在することが従う。
この自己同型群の存在から、モジュラー函数のある特殊値たちが代数的数であることを
構成的でない方法で証明できる。
この命題はZF内で別の方法(構成的)によっても証明できるが、二つの事実は当然矛盾しない。
という話を、藤原一宏という先生が書いていた。