Number theory

Euler’s theorem: modulo 10

Every unit modulo 10 raised to the fourth power returns to 1. Exhaust a finite type with a kernel-checked proof.

-- Top 100 #10: Euler’s theorem: modulo 10
-- History: 1760 · Euler; 1640 · Fermat.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: Modulo 10, the invertible residues are exactly 1, 3, 7, and 9.
-- Scope: Checks Euler’s theorem for every residue modulo 10 coprime to 10. This is not the theorem for arbitrary moduli.
-- Source: https://lurch.plus/100/

-- phi(10) = 4: four residues are coprime to 10.
theorem euler_mod_ten :
    ∀ a : Fin 10, Nat.gcd a.val 10 = 1 → a^4 = 1 := by
  decide

#eval (7 : Fin 10)^4

Explanation

`theorem / example`

A named theorem or anonymous example states exactly the claim Lean must check. Read its inputs and assumptions to see the scope.

`decide`

Builds a proof using a decision procedure. Quantifying over Fin n checks every one of its finitely many values.

`Fin n`

Fin n contains the natural numbers less than n, each with a bound proof. Addition and multiplication wrap modulo n.

Background and proof scope

1760 · Euler; 1640 · Fermat

Modulo 10, the invertible residues are exactly 1, 3, 7, and 9.

Checks Euler’s theorem for every residue modulo 10 coprime to 10. This is not the theorem for arbitrary moduli.

Historical Top 100 list (reproduced by Lurch)

Expected output

Reference only. Run the file to check its actual result.

Exercise

Try modulus 12, which also has four invertible residues. Update the modulus in the theorem and the #eval command.