English
φ(n) multiplied by the product of the primes dividing n equals n multiplied by the product of (p−1) over those primes.
Русский
φ(n), умноженная на произведение простых, делящих n, равна n, умноженному на произведение (p−1) по этим простым.
LaTeX
$$$$ \\varphi(n) \\prod_{p \\in n.primeFactors} p = n \\prod_{p \\in n.primeFactors} (p-1). $$$$
Lean4
/-- Euler's product formula for the totient function. -/
theorem totient_mul_prod_primeFactors (n : ℕ) : (φ n * ∏ p ∈ n.primeFactors, p) = n * ∏ p ∈ n.primeFactors, (p - 1) :=
by
by_cases hn : n = 0; · simp [hn]
rw [totient_eq_prod_factorization hn]
nth_rw 3 [← factorization_prod_pow_eq_self hn]
simp only [prod_primeFactors_prod_factorization, ← Finsupp.prod_mul]
refine Finsupp.prod_congr (M := ℕ) (N := ℕ) fun p hp => ?_
rw [Finsupp.mem_support_iff, ← zero_lt_iff] at hp
rw [mul_comm, ← mul_assoc, ← pow_succ', Nat.sub_one, Nat.succ_pred_eq_of_pos hp]
