totient_eq_prod_factorization — Mathlib

English

Let n > 0. The totient φ(n) equals the product over primes p with their exponents k in n of p^(k-1)(p-1).

Русский

Пусть n > 0. φ(n) равняется произведению по простым p, входящим в факторизацию n, p^(k-1)(p-1) для соответствующей степени k.

LaTeX

$$$$ \\\\varphi(n) = \\\\prod_{p^k \\\\parallel n} p^{k-1}(p-1) $$$$

Lean4

/-- Euler's product formula for the totient function. -/
theorem totient_eq_prod_factorization {n : ℕ} (hn : n ≠ 0) :
    φ n = n.factorization.prod fun p k => p ^ (k - 1) * (p - 1) :=
  by
  rw [multiplicative_factorization φ (@totient_mul) totient_one hn]
  apply Finsupp.prod_congr _
  intro p hp
  have h := zero_lt_iff.mpr (Finsupp.mem_support_iff.mp hp)
  rw [totient_prime_pow (prime_of_mem_primeFactors hp) h]

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