Comparing remainders

Two integers can differ while having the same remainder.

Start with a concrete example

Share eight sweets among three people. Each gets two, with two sweets left. Now change the number of sweets.

Move the number or condition

8 = 3 × 2 + 2. Remainder 2.

How this example differs from the definition

This is ordinary division of whole numbers. The proof also uses more structured arithmetic objects.

Compare the numbers in the question with the diagram you are moving. You can try again.

What remains when 8 sweets are shared in whole pieces among 3 people?

Read the answer and reasoning

2 sweets. Give each person 2: 6 are used, and 8 − 6 = 2 remain. In the diagram, set the number to 8.

Divide an integer by a positive integer n and retain its remainder.
Two integers are congruent modulo n when their difference is divisible by n; for ordinary integers this is the same remainder test.
ZMod n packages arithmetic modulo n. When n is prime, every nonzero residue can be used as a divisor.

7 and 2 both leave remainder 2 on division by 5. Their difference 5 is divisible by 5.

Mathlib · db584cd · Defs.lean

142def ZMod : ℕ → Type143  | 0 => ℤ144  | n + 1 => Fin (n + 1)

For n + 1, Fin (n + 1) provides the finite set of residues. The special case ZMod 0 is ℤ; the remainder example above uses a positive modulus.