前回疑問に思ったことはまだ解決していません。なので今回は疑問となぜそう思ったのかだけを書いておきます。 前回までの記事でgaussIntは可換環であることを示しました。またgaussIntにquotientやremainderを定義し除法の原理を示すことでEuclideanDomainという型であることも示しました。しかし特に後者の証明ではガウス整数用の（いわゆる）ユークリッド関数を構成してそれが除法の原理を満たすことを示しただけでした。 ガウス整数が整域であること（零因子がないこと）は別途示す必要があると思っていたので、それなしで証明が終わったことが疑問だったのです。 もちろんその証明は普通…
