funlean.
Step 11 / 64

High school

Division on a clock

Coprime to the clock size means a true inverse: a · a⁻¹ = 1 on the residue world.

Start with a concrete example

On a 9-mark clock, multiplying 2 by 5 gives 10, which lands at 1. So multiplying by 5 undoes multiplying by 2. Multiples of 3 land only at 0,3,6, never 1.

A small check: try the idea

Think with the concrete example above. You can try again.

On the 9-mark remainder clock, why does 5 undo multiplication by 2?

Read the answer and reasoning

2×5=10 lands at 1. Undoing multiplication uses a product equal to 1 in that arithmetic: 10 leaves 1 after division by 9.

Build the idea in three steps

  1. On a clock of size five, the product 2 × 3 = 6 = 1: the multiplication returns exactly to one. When that happens, 3 undoes 2 — division has come home to the clock, and 3 is written a⁻¹.
  2. The function inv in the excerpt gives a⁻¹ on every clock, and its docstring carries the precise promise: a * a⁻¹ = gcd a.val n. Only when gcd equals one — with a coprime to the clock size — does the product really return to one.
  3. Prime clocks are the generous ones: any nonzero card is coprime to a prime p, so on ℤ/pℤ division works everywhere except at zero. Composite clocks ration it out. This is the world where the proof reduces curves (traceOfFrobenius counts in exactly such a world).

A small example

The nine-clock turns the trick down but not off: 2⁻¹ = 5 there, since 2 × 5 = 10 = 1 (gcd 2 9 = 1). But 3 has no inverse on it: every multiple of 3 lands on 0, 3 or 6 — never on 1, because gcd 3 9 = 3.

Lean definition · original excerpt

Mathlib · db584cd · Basic.lean

/-- The inversion on `ZMod n`.It is setup in such a way that `a * a⁻¹` is equal to `gcd a.val n`.In particular, if `a` is coprime to `n`, and hence a unit, `a * a⁻¹ = 1`. -/def inv : ∀ n : ℕ, ZMod n → ZMod n  | 0, i => Int.sign i  | n + 1, i => Nat.gcdA i.val (n + 1) instance (n : ℕ) : Inv (ZMod n) :=  ⟨inv n⟩

How to read this Lean

Behind inv stands the extended Euclidean bookkeeping (Nat.gcdA): it finds s with a · val + k · n = gcd, and dividing that identity by n inside the clock leaves a * a⁻¹ = gcd. The word unit — an element with a true inverse — is the same word the Eisenstein world uses for its six rotations and the endgame worlds use for their invertible elements. From this page on, invertible has one meaning everywhere.

Original source ↗ · L709–717Open the complete saved source

Where this idea is used

12. The workshops agree13. Pip’s impossible quilt
I’m lost · Help

Mika’s help desk

Division on a clock

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

Coprime to the clock size means a true inverse: a · a⁻¹ = 1 on the residue world.

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

A small clue

The nine-clock turns the trick down but not off: 2⁻¹ = 5 there, since 2 × 5 = 10 = 1 (gcd 2 9 = 1). But 3 has no inverse on it: every multiple of 3 lands on 0, 3 or 6 — never on 1, because gcd 3 9 = 3.

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 →