prod_primeFactors — Mathlib

English

For a squarefree l, the product of f over the prime factors of l equals f(l).

Русский

Для квадратно-безповторного $l$ произведение $f(p)$ по простым делителям $l$ равно $f(l)$.

LaTeX

$$$\prod_{p\in l.{\rm primeFactors}} f(p) = f(l) \quad\text{если } l\text{ квадратно-безповторно}$$$

Lean4

theorem prod_primeFactors [CommMonoidWithZero R] {f : ArithmeticFunction R} (h_mult : f.IsMultiplicative) {l : ℕ}
    (hl : Squarefree l) : ∏ a ∈ l.primeFactors, f a = f l := by
  rw [← h_mult.map_prod_of_subset_primeFactors l _ Finset.Subset.rfl, prod_primeFactors_of_squarefree hl]

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