3段階で考えよう
- まず世界の大きさとして正の整数nを決めます。中に置けるのは、nで割った余り0・1・…・n − 1だけです。
- 余りどうしの足し算は、和をnで割った余りで置き換えます。引き算とかけ算も同じ方法で決まります。
- この構成を「nを法とする整数」と呼びます。LeanではZMod nで、0の場合はℤ、正のnの場合はFin nという有限の余りの集合です。
小さな例で確かめる
0・…・11の目盛りの時計では、9時の5時間後は2時。9 + 5 = 14で、14を12で割ると余り2です。
順番 9 / 64
中学校
時計の算術
余りの集合を決め、その中だけで計算する世界を作ります。
まず、身近な例で
あめ8個を3人に同じ数ずつ配ると、1人2個ずつで、2個余ります。あめの数を変えてみよう。
8 = 3 × 2 + 2。余りは2個。
この例と、本当の定義の違い
これは整数の割り算の例です。証明では、もっと構造を持つ数の対象にも同じ考え方を使います。
ちいさな確認：考えてみよう
問いの数と、今動かしている図の数を見比べよう。何度やり直しても大丈夫。
8 = 3×2+2、5 = 3×1+2。もとの数が違っても、余りは同じになります。
この確認では、説明に合う答えを選べました。漫画の中でも、同じ考え方を探してみよう。
答えと考え方を読む
はい、両方とも2。 8 = 3×2+2、5 = 3×1+2。もとの数が違っても、余りは同じになります。
Leanの定義・原文の抜粋
Mathlib · db584cd · Defs.lean
/-- The integers modulo `n : ℕ`. -/@[to_additive_dont_translate]def ZMod : ℕ → Type| 0 => ℤ
このLeanの読み方
定義は二つの場合をそのまま並べます。ZMod 0はℤ、ZMod (n + 1)はFin (n + 1)。時計の例は正の大きさなので、世界は有限です。