$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 ガウス整数を構成する」では2つの整数のペアの形の構造体としてガウス整数を定義します。 @[ext]structure gaussInt where re : ℤ im : ℤ @[ext…