totient_eq_div_primeFactors_mul — Mathlib

English

φ(n) equals (n divided by the product of its prime factors) multiplied by the product of (p−1) over those primes.

Русский

φ(n) равняется (n делится на произведение простых делителей n) умноженному на произведение (p−1) по этим простым.

LaTeX

$$$$ \\varphi(n) = \\frac{n}{\\prod_{p \\in n.primeFactors} p} \\cdot \\prod_{p \\in n.primeFactors} (p-1). $$$$

Lean4

/-- Euler's product formula for the totient function. -/
theorem totient_eq_div_primeFactors_mul (n : ℕ) : φ n = (n / ∏ p ∈ n.primeFactors, p) * ∏ p ∈ n.primeFactors, (p - 1) :=
  by
  rw [← mul_div_left n.totient, totient_mul_prod_primeFactors, mul_comm, Nat.mul_div_assoc _ (prod_primeFactors_dvd n),
    mul_comm]
  exact prod_pos (fun p => pos_of_mem_primeFactors)

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