prodPrimeFactors_apply — Mathlib

English

For n ≠ 0, ∏_{p ∣ n} f(p) equals ∏_{p ∈ n.primeFactors} f(p).

Русский

Для n ≠ 0, произведение по простым делителям n равно произведению по элементам primeFactors(n).

LaTeX

$$$$ \prod_{p \mid n} f(p) = \prod_{p \in n.primeFactors} f(p) \quad (n \neq 0) $$$$

Lean4

@[simp]
theorem prodPrimeFactors_apply [CommMonoidWithZero R] {f : ℕ → R} {n : ℕ} (hn : n ≠ 0) :
    ∏ᵖ p ∣ n, f p = ∏ p ∈ n.primeFactors, f p :=
  if_neg hn

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