English
Euler's product formula for φ expressed in rational numbers: φ(n) as a rational equals n times the product over primes p dividing n of (1 − 1/p).
Русский
Формула Эйлера для φ выражается в рациональных числах: φ(n) как рациональное число равно n, умноженному на произведение по простым p, делящим n, (1 − 1/p).
LaTeX
$$$$ (\varphi(n) \in \mathbb{Q}) \;=\; n \prod_{p \in n.primeFactors} \\left(1 - \\frac{1}{p}\\right). $$$$
Lean4
/-- Euler's product formula for the totient function. -/
theorem totient_eq_mul_prod_factors (n : ℕ) : (φ n : ℚ) = n * ∏ p ∈ n.primeFactors, (1 - (p : ℚ)⁻¹) :=
by
by_cases hn : n = 0
· simp [hn]
have hn' : (n : ℚ) ≠ 0 := by simp [hn]
have hpQ : (∏ p ∈ n.primeFactors, (p : ℚ)) ≠ 0 :=
by
rw [← cast_prod, cast_ne_zero, ← zero_lt_iff, prod_primeFactors_prod_factorization]
exact prod_pos fun p hp => pos_of_mem_primeFactors hp
simp only [totient_eq_div_primeFactors_mul n, prod_primeFactors_dvd n, cast_mul, cast_prod, cast_div_charZero,
mul_comm_div, mul_right_inj' hn', div_eq_iff hpQ, ← prod_mul_distrib]
refine prod_congr rfl fun p hp => ?_
have hp := pos_of_mem_primeFactorsList (List.mem_toFinset.mp hp)
have hp' : (p : ℚ) ≠ 0 := cast_ne_zero.mpr hp.ne.symm
rw [sub_mul, one_mul, mul_comm, mul_inv_cancel₀ hp', cast_pred hp]
