足し算とかけ算の仕組み

足し算とかけ算の規則をそろえると、別の数の世界を同じ言葉で比べられます。

まず、身近な例で

リンゴ2個とナシ4個入りの袋が3袋。全部で3×(2+4)=18個。種類ごとに数えても3×2+3×4=18個です。「環」では、足し算と掛け算がこのような規則を守ります。

上の具体例を見ながら考えよう。何度やり直しても大丈夫。

リンゴ2個とナシ4個の袋が3袋。全部で何個？

答えと考え方を読む

18個。両方の種類を3袋ぶん数えて、3×2+3×4=6+12=18。リンゴだけを3倍すると、ナシを数え落とします。

時計の世界では、同じ余りの集合に足し算とかけ算という二つの操作があります。
共有する規則の一覧、たとえば(a + b) + c = a + (b + c)やa × (b + c) = a × b + a × cが、その操作が満たすべきことを正確に決めます。
二つの操作がその規則に従う集合が環です。Leanはかけ算の順序が入れ替わる場合をCommRingと呼び、ライブラリは余りの集合Fin nにまさにその構造を記録します。

余りを取っても規則は保たれます。5の時計では、3 × (2 + 4)と(3 × 2) + (3 × 4)はどちらも3になります。

Mathlib · db584cd · Defs.lean

126def instCommRing (n : ℕ) [NeZero n] : CommRing (Fin n) where127  intCast n := Fin.intCast n

instCommRingは、余りの集合Fin nがCommRingを持つことを述べています。見えている欄のintCastは、普通の整数をその中に入れる方法を供給し、残りの規則も同じ構造の欄です。