pow_totient — Mathlib

English

For any x with gcd(x,n)=1, x^φ(n) ≡ 1 (mod n).

Русский

Для любого x взаимно простого с n верно x^φ(n) ≡ 1 (mod n).

LaTeX

$$$x^{\\varphi(n)} \\equiv 1 \\pmod n \\quad\\text{whenever } \\gcd(x,n)=1$$$

Lean4

/-- The **Fermat-Euler totient theorem**. `Nat.ModEq.pow_totient` is an alternative statement
  of the same theorem. -/
@[simp]
theorem pow_totient {n : ℕ} (x : (ZMod n)ˣ) : x ^ φ n = 1 :=
  by
  cases n
  · rw [Nat.totient_zero, pow_zero]
  · rw [← card_units_eq_totient, pow_card_eq_one]

Похожие утверждения