English
The sum of φ(d) over all positive divisors d of n equals n.
Русский
Сумма φ(d) по всем делителям d числа n равна n.
LaTeX
$$$$\sum_{d \mid n} φ(d) = n.$$$$
Lean4
/-- For `d ∣ n`, the totient of `n/d` equals the number of values `k < n` such that `gcd n k = d` -/
theorem totient_div_of_dvd {n d : ℕ} (hnd : d ∣ n) : φ (n / d) = #({k ∈ range n | n.gcd k = d}) :=
by
rcases d.eq_zero_or_pos with (rfl | hd0); · simp [eq_zero_of_zero_dvd hnd]
rcases hnd with ⟨x, rfl⟩
rw [Nat.mul_div_cancel_left x hd0]
apply Finset.card_bij fun k _ => d * k
· simp only [mem_filter, mem_range, and_imp, Coprime]
refine fun a ha1 ha2 => ⟨by gcongr, ?_⟩
rw [gcd_mul_left, ha2, mul_one]
· simp [hd0.ne']
· simp only [mem_filter, mem_range, exists_prop, and_imp]
refine fun b hb1 hb2 => ?_
have : d ∣ b := by
rw [← hb2]
apply gcd_dvd_right
rcases this with ⟨q, rfl⟩
refine ⟨q, ⟨⟨(mul_lt_mul_iff_right₀ hd0).1 hb1, ?_⟩, rfl⟩⟩
rwa [gcd_mul_left, mul_eq_left hd0.ne'] at hb2
