Build the idea in three steps
- In the clock world, arithmetic has two operations on the same set of residues: addition and multiplication.
- A shared list of rules, such as (a + b) + c = a + (b + c) and a × (b + c) = a × b + a × c, fixes exactly what those operations must obey.
- A set carrying both operations under those rules is a ring. Lean names the commutative version CommRing, and the library records precisely that structure for the residues Fin n.
A small example
Taking remainders does not break the rules: for the 5-clock, 3 × (2 + 4) and (3 × 2) + (3 × 4) both become 3.