prodPrimeFactors_one_sub_of_squarefree

English

For squarefree n and multiplicative f, ∏_{p|n} (1 − f(p)) = ∑_{d|n} μ(d) f(d).

Русский

Для квадратноразложимого n и умножаемой f: ∏_{p|n} (1 − f(p)) = ∑_{d|n} μ(d) f(d).

LaTeX

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

Lean4

theorem prodPrimeFactors_one_sub_of_squarefree [CommRing R] (f : ArithmeticFunction R) (hf : f.IsMultiplicative) {n : ℕ}
    (hn : Squarefree n) : ∏ p ∈ n.primeFactors, (1 - f p) = ∑ d ∈ n.divisors, μ d * f d :=
  by
  trans (∏ p ∈ n.primeFactors, (1 + (ArithmeticFunction.pmul (μ : ArithmeticFunction R) f) p))
  · apply Finset.prod_congr rfl; intro p hp
    rw [pmul_apply, intCoe_apply,
      ArithmeticFunction.moebius_apply_prime (prime_of_mem_primeFactorsList (List.mem_toFinset.mp hp))]
    ring
  · rw [(isMultiplicative_moebius.intCast.pmul hf).prodPrimeFactors_one_add_of_squarefree hn]
    simp_rw [pmul_apply, intCoe_apply]

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