English
For any natural n and function f, the product over divisors d of n of f(n/d) equals the product over divisors d of n of f(d).
Русский
Для любого n и функции f произведение по делителям d на n/d равно произведению по делителям d на d.
LaTeX
$$$\displaystyle \prod_{d \mid n} f(n/d) = \prod_{d \mid n} f(d).$$$
Lean4
@[to_additive (attr := simp) sum_div_divisors]
theorem prod_div_divisors {α : Type*} [CommMonoid α] (n : ℕ) (f : ℕ → α) :
(∏ d ∈ n.divisors, f (n / d)) = n.divisors.prod f :=
by
by_cases hn : n = 0; · simp [hn]
rw [← prod_image]
· exact prod_congr (image_div_divisors_eq_divisors n) (by simp)
· intro x hx y hy h
rw [mem_coe, mem_divisors] at hx hy
exact (div_eq_iff_eq_of_dvd_dvd hn hx.1 hy.1).mp h
