funlean.
Step 9 / 64

Middle school

Clock arithmetic

Computing inside a fixed finite set of residues is a number world of its own.

Start with a concrete example

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

Groups of 32Left: 2

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.

A small check: try the idea

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

Do 8 and 5 land on the same remainder when divided by 3?

Read the answer and reasoning

Yes, both leave 2. 8 = 3×2+2 and 5 = 3×1+2. Full numbers can differ while remainders agree.

Build the idea in three steps

  1. Decide one positive size n first. The only numbers the world contains are the n remainders of division by n: 0, 1, …, n − 1.
  2. Adding two residues means replacing their sum by its remainder on division by n. Subtraction and multiplication are decided the same way.
  3. The construction is called the integers modulo n. In Lean it is ZMod n: for the case 0 it is ℤ, and for a positive n it is the finite set Fin n.

A small example

On a clock labelled 0, …, 11, five hours after nine is two: 9 + 5 = 14 and 14 leaves remainder 2 on division by 12.

Lean definition · original excerpt

Mathlib · db584cd · Defs.lean

/-- The integers modulo `n : ℕ`. -/@[to_additive_dont_translate]def ZMod : ℕ → Type  | 0 => ℤ

How to read this Lean

The definition lists the two cases directly: ZMod 0 is ℤ, and ZMod (n + 1) is Fin (n + 1). The clock example uses a positive size, so its world is finite.

Original source ↗ · L140–143Open the complete saved source

Where this idea is used

2. The case of three5. The suspicious parcel7. The veterans’ cabinet8. The secret duet9. Two doors to the concert10. A three-note audition11. Borrow a better passport12. The workshops agree13. Pip’s impossible quilt14. The shrinking reservation
I’m lost · Help

Mika’s help desk

Clock arithmetic

One thing at a time

Read the three explanation steps first. The Lean source is there for a closer look afterwards; you do not have to read it first.

In simpler words

Computing inside a fixed finite set of residues is a number world of its own.

Earlier ideas are listed under “Start with these ideas” on this page.

A small clue

On a clock labelled 0, …, 11, five hours after nine is two: 9 + 5 = 14 and 14 leaves remainder 2 on division by 12.

Close this panel to return to the exact place you were reading. These are prepared hints for this page.

Start with the first small story →