sum_divisors — Mathlib

English

If n > 0 and n = ∏ p^{a_p}, then the sum of divisors σ(n) equals ∏_{p ∣ n} (∑_{i=0}^{a_p} p^{i}).

Русский

Пусть n > 0 и n = ∏ p^{a_p}. Тогда сумма делителей σ(n) равна ∏_{p ∣ n} (∑_{i=0}^{a_p} p^{i}).

LaTeX

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

Lean4

theorem _root_.Nat.sum_divisors {n : ℕ} (hn : n ≠ 0) :
    ∑ d ∈ n.divisors, d = ∏ p ∈ n.primeFactors, ∑ k ∈ .range (n.factorization p + 1), p ^ k :=
  by
  rw [← sigma_one_apply, isMultiplicative_sigma.multiplicative_factorization _ hn]
  exact
    Finset.prod_congr n.support_factorization fun _ h => sigma_one_apply_prime_pow <| Nat.prime_of_mem_primeFactors h

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