3段階で考えよう
- 整数を正の整数nで割り、余りを残します。
- 差がnで割り切れる二つの整数を、nを法として合同と言います。普通の整数では、余りが同じという判定です。
- ZMod nはnを法とする計算の仕組み。nが素数なら、0でない余りの数で割る操作もできます。
小さな例で確かめる
7も2も、5で割ると余り2。差の5は5で割り切れます。
順番 8 / 64
中学校
余りで比べる・合同
数が違っていても、割った余りが同じなら合同です。
まず、身近な例で
あめ8個を3人に同じ数ずつ配ると、1人2個ずつで、2個余ります。あめの数を変えてみよう。
8 = 3 × 2 + 2。余りは2個。
この例と、本当の定義の違い
これは整数の割り算の例です。証明では、もっと構造を持つ数の対象にも同じ考え方を使います。
ちいさな確認：考えてみよう
問いの数と、今動かしている図の数を見比べよう。何度やり直しても大丈夫。
1人2個ずつで6個使い、8 − 6 = 2個余ります。図の数を8にして数えてみよう。
この確認では、説明に合う答えを選べました。漫画の中でも、同じ考え方を探してみよう。
答えと考え方を読む
2個。 1人2個ずつで6個使い、8 − 6 = 2個余ります。図の数を8にして数えてみよう。
Leanの定義・原文の抜粋
Mathlib · db584cd · Defs.lean
def ZMod : ℕ → Type| 0 => ℤ| n + 1 => Fin (n + 1)
このLeanの読み方
n + 1の場合はFin (n + 1)という有限の余りの集合を使います。特別にZMod 0はℤです。上の余りの例は、正の数で割る場合です。