English
For coprime x and n, x^φ(n) ≡ 1 [MOD n].
Русский
Для взаимно простых x и n верно x^φ(n) ≡ 1 [MOD n].
LaTeX
$$$x^{\\varphi(n)} \\equiv 1 \\pmod n \\quad\\text{если } \\gcd(x,n)=1$$$
Lean4
/-- The **Fermat-Euler totient theorem**. `ZMod.pow_totient` is an alternative statement
of the same theorem. -/
theorem pow_totient {x n : ℕ} (h : Nat.Coprime x n) : x ^ φ n ≡ 1 [MOD n] :=
by
rw [← ZMod.natCast_eq_natCast_iff]
let x' : Units (ZMod n) := ZMod.unitOfCoprime _ h
have := ZMod.pow_totient x'
apply_fun ((fun (x : Units (ZMod n)) => (x : ZMod n)) : Units (ZMod n) → ZMod n) at this
simpa only [Nat.succ_eq_add_one, Nat.cast_pow, Units.val_one, Nat.cast_one, coe_unitOfCoprime,
Units.val_pow_eq_pow_val]
