$i$を虚数単位とします。つまり$i=\sqrt{-1}$です。このときガウス整数とは$a+b\,i,\, a,b\in\mathbb{Z}$という形をした複素数をガウス整数と呼びます。虚部と実部が整数であるような複素数のことです。例えば$-3i,\, 17+38i$はいずれもガウス整数です。一方$\frac{1}{2}+4i$はガウス整数ではありません。
Mathematics In Lean 4の「6.3 ガウス整数を構成する」では２つの整数のペアの形の構造体としてガウス整数を定義します。
@[ext]
structure gaussInt where
re : ℤ
im : ℤ
@[ext]というアノテーション(Lean言語として注釈)を付けることでこの構造体のインスタンス間の等号は構造体の構成要素の等号によって定義されることや、それによって成り立つ定理が自動生成されます。
ガウス整数には加法、減法、乗法及び加法の単位元0、乗法の単位元1が自然に定義されます。またプログラム（定理や証明）をLean4で書く際にこれらの記法が+, -, *, 0, 1と記述でき、簡単な簡約ルールが動作するように定理を準備すると便利です。この辺は単純で繰り返しが多いので「6.3 ガウス整数を構成する」のプログラム部分を見てみてください。
ほとんど自明ではあるのですが、このように定義したガウス整数が可換環であることを簡単に示すことができます。可換環では加法、減法、乗法および加法の単位元、乗法の単位元とそれらの間の演算、乗法の可換性、乗法と加法の分配法則などを示すことが必要です。実際に示すべきことをまとめてLean4が教えてくれます。
instance : CommRing gaussInt := _
と記述して、このときにエディタが表示する印をクリックすると'_'の部分に（結構大きな）テンプレートが表示されます。その冒頭を示します。
instance : CommRing gaussInt where
add := _
add_assoc := _
zero := _
zero_add := _
add_zero := _
nsmul := _
nsmul_zero := _
nsmul_succ := _
add_comm := _
mul := _
left_distrib := _
right_distrib := _テンプレートはこの３倍くらい続きます。
このテンプレートの中の'_'の部分を埋めていくことでgaussIntがCommRingであることを示していきます。まずadd, zero, mulなどはgaussIntの定義をもってくることがそれらの証明になります。次にadd_assoc, add_comm, left_distrib, zero_add, add_zeroなどが成り立つことを証明していきます。'_'の後にbyをいれてからgaussIntの演算の性質を使って証明を進めます。とは言ってもほとんど自明で証明自体同じパターンで進めることができます。
nsmul, nsmul_zero, nsmul_succは自然数と可換環の要素との演算です。これらは無くてもガウス整数が可換環になることの証明には関係ないので一旦忘れてください。
これを埋めてgaussIntがCommRingのすべての性質を持つことが証明できました。
重要な可換環は非自明です。ここで非自明とは$0\ne 1$であり少なくとも要素を２つ持つということを意味します。
gaussIntでも$0\ne 1$が成り立つことを示し、それをシステムに教えてあげることにします。こうすることでLean4はこれ以降gaussIntは非自明であることを知って、それを前提とした定理が成り立つことも知りながら証明アシストしてくれるようになります。
instance : Nontrivial gaussInt := by
use 0, 1
rw [Ne, gaussInt.ext_iff]
simp
