>>504
>系3.12に選択公理って使ってるの？
>別にそれは問題でも何でも無いけど

個人的感想で 根拠薄弱だが
系3.12に選択公理は、間接的には使っているが
直接的には使っていないと思う

直接的な使用は気付かなかったし 過去話題なっていない
が
間接的には 使っていてもおかしくないし
IUTは 20世紀の膨大な代数学、代数幾何、数論幾何の蓄積の上にある
そのどこかで 使っているのでは？ しらんけど （＾＾
”使っていない”を立証するには それこそ LEANの検証要だろう？