Remainder families

Dividing by $k$ splits the integers into exactly $k$ families — the integers with remainder $0$, with remainder $1$, …, with remainder $k - 1$. Every integer belongs to exactly one family. A splitting like this, into non-overlapping pieces that together cover everything, is called a partition.

The rule "same remainder" has three properties:

• every integer is related to itself (reflexive);
• if $a$ is related to $b$, then $b$ is related to $a$ (symmetric);
• if $a$ is related to $b$ and $b$ to $c$, then $a$ is related to $c$ (transitive).

A relation with these properties is an equivalence relation, and its families are called equivalence classes. Every equivalence relation gives a partition, and every partition comes from one.

/-- Congruence modulo `k` is an **equivalence relation** (reflexive, symmetric, transitive).
Its equivalence classes are the "hours" on a `k`-hour clock. -/
theorem modEq_equivalence (k : Int) : Equivalence (ModEq k) :=
  ⟨modEq_refl k, modEq_symm, modEq_trans⟩

Now the surprise from the experiment. If $a \equiv a'$ and $b \equiv b' \pmod{k}$, then $a + b \equiv a' + b'$. Why? Because $a - a'$ and $b - b'$ are multiples of $k$, so their sum $(a + b) - (a' + b')$ is too. The family of a sum depends only on the families. The same is true for products.

That means we can add and multiply the families themselves. The families become the elements of a new number system, written $\Z/k\Z$ — a quotient of $\Z$. Building new structures by "gluing together" equivalent elements, and checking that the operations are well defined, is one of the most-used constructions in all of algebra.

/-- You may reduce before or after adding: `(a mod k + b mod k) mod k = (a + b) mod k`.
This applies core Lean's `Nat.add_mod`. -/
theorem mod_add_mod (a b k : Nat) : (a % k + b % k) % k = (a + b) % k :=
  (Nat.add_mod a b k).symm