前回疑問に思ったことはまだ解決していません。なので今回は疑問となぜそう思ったのかだけを書いておきます。
前回までの記事でgaussIntは可換環であることを示しました。またgaussIntにquotientやremainderを定義し除法の原理を示すことでEuclideanDomainという型であることも示しました。しかし特に後者の証明ではガウス整数用の（いわゆる）ユークリッド関数を構成してそれが除法の原理を満たすことを示しただけでした。
ガウス整数が整域であること（零因子がないこと）は別途示す必要があると思っていたので、それなしで証明が終わったことが疑問だったのです。
もちろんその証明は普通の意味では簡単です。複素数は体なので整域です。ガウス整数はその部分集合なのでここに零因子があればそれは複素数に零因子があることになり整域であることと矛盾します。
一方今回の証明ではgaussIntがLean4の組み込みの複素数の部分集合という形では定義していません。あくまで２つの整数の組みとして定義して加減乗除余などを個別に定義している構造です。この構造が整域になることを示すのは（それも簡単ではありますが）個別に必要だと思ったのです。しかしそのようなことはなく、commRingにquotientやremainderを定義しているだけで特に零因子がないことは明示的には証明されていません。
なぜこれで良いのか少しだけ調べてみました。Mathlib/EuclideanDomain/Defs.leanにあるEucledianDomainの定義を見るとこんな感じです。
class EuclideanDomain (R : Type u) extends CommRing R, Nontrivial R where
/-- A division function (denoted `/`) on `R`.
This satisfies the property `b * (a / b) + a % b = a`, where `%` denotes `remainder`. -/
protected quotient : R → R → R
/-- Division by zero should always give zero by convention. -/
protected quotient_zero : ∀ a, quotient a 0 = 0
/-- A remainder function (denoted `%`) on `R`.
This satisfies the property `b * (a / b) + a % b = a`, where `/` denotes `quotient`. -/
protected remainder : R → R → R
/-- The property that links the quotient and remainder functions.
This allows us to compute GCDs and LCMs. -/
protected quotient_mul_add_remainder_eq : ∀ a b, b * quotient a b + remainder a b = a
/-- A well-founded relation on `R`, satisfying `r (a % b) b`.
This ensures that the GCD algorithm always terminates. -/
protected r : R → R → Prop
/-- The relation `r` must be well-founded.
This ensures that the GCD algorithm always terminates. -/
r_wellFounded : WellFounded r
/-- The relation `r` satisfies `r (a % b) b`. -/
protected remainder_lt : ∀ (a) {b}, b ≠ 0 → r (remainder a b) b
/-- An additional constraint on `r`. -/
mul_left_not_lt : ∀ (a) {b}, b ≠ 0 → ¬r (a * b) a
つまり非自明($0\ne 1$)なcommRingにこれらの関数と関係と制約を導入すればEuclideanDomainになるということです。ひょっとして可換環にユークリッド関数と除法の原理を足せば零因子がないことが証明できるのでしょうか、、、
あぁ、上の段落を書きながら零因子があるとmul_left_not_ltが成り立たないことに気がつきました。$a, b$を零因子、すなわち$a\ne 0, b\ne 0, a * b=0$とします。$a * b = 0$及び$r\; 0\; a$から$r\; (a*b)\; a$。これはmul_left_not_lt a bに矛盾します。これで無事に任意のEuclideanDomainには零因子がないこと、すなわち整域であることが証明できました。
お騒がせしました、、、
