prodPrimeFactors_one_add_of_squarefree

English

For a multiplicative function f, and squarefree n, the product over primes dividing n of (1 + f(p)) equals the sum over divisors d of n of f(d).

Русский

Для умножаемой функции f и квадратноразложимого числа n выполнено тождество: ∏_{p|n} (1 + f(p)) = ∑_{d|n} f(d).

LaTeX

$$∏_{p ∈ n.primeFactors} (1 + f(p)) = ∑_{d ∈ n.divisors} f(d)$$

Lean4

theorem prodPrimeFactors_one_add_of_squarefree [CommSemiring R] {f : ArithmeticFunction R} (h_mult : f.IsMultiplicative)
    {n : ℕ} (hn : Squarefree n) : ∏ p ∈ n.primeFactors, (1 + f p) = ∑ d ∈ n.divisors, f d :=
  by
  trans (∏ᵖ p ∣ n, ((ζ : ArithmeticFunction R) + f) p)
  · simp_rw [prodPrimeFactors_apply hn.ne_zero, add_apply, natCoe_apply]
    apply Finset.prod_congr rfl; intro p hp
    rw [zeta_apply_ne (prime_of_mem_primeFactorsList <| List.mem_toFinset.mp hp).ne_zero, cast_one]
  rw [isMultiplicative_zeta.natCast.prodPrimeFactors_add_of_squarefree h_mult hn, coe_zeta_mul_apply]

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