sigma_eq_prod_primeFactors_sum_range_factorization_pow_mul

English

Let n > 0 be an integer with prime factorization n = ∏ p^{a_p}. For every natural number k, the divisor-sum function σ_k satisfies σ_k(n) = ∏_{p ∣ n} (∑_{i=0}^{a_p} p^{i k}).

Русский

Пусть n > 0 имеет простейшее разложение n = ∏ p^{a_p}. Тогда для любого k ∈ ℕ выполнено σ_k(n) = ∏_{p ∣ n} ∑_{i=0}^{a_p} p^{i k}.

LaTeX

$$$$\sigma_k(n) = \prod_{p \mid n} \left( \sum_{i=0}^{a_p} p^{i k} \right)$$$$

Lean4

theorem sigma_eq_prod_primeFactors_sum_range_factorization_pow_mul {k n : ℕ} (hn : n ≠ 0) :
    σ k n = ∏ p ∈ n.primeFactors, ∑ i ∈ .range (n.factorization p + 1), p ^ (i * k) :=
  by
  rw [isMultiplicative_sigma.multiplicative_factorization _ hn]
  exact Finset.prod_congr n.support_factorization fun _ h ↦ sigma_apply_prime_pow <| Nat.prime_of_mem_primeFactors h

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