Eulers_Theorem_v2

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

euler-theoremmodular-arithmeticnumber-theoryproofwiki

Let $a, m \in \Z$ be coprime integers: $a \perp m$ . Let $\map \phi m$ be the Euler $\phi$ function of $m$ . Then $a^{\map \phi m} \equiv 1 \pmod m$

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.Data.ZMod.Basic
import Mathlib.Data.Nat.Totient

Formal statement

theorem Eulers_Theorem_v2 (a m : ℕ) (hm : 0 < m) (hcop : Nat.Coprime a m) : a ^ Nat.totient m ≡ 1 [MOD m] := by sorry

Source