not_dvd_finsuppProd — Mathlib

English

If for all a in the support of f, p ∤ g a (f a), then p ∤ f.prod g.

Русский

Если для каждого элемента в опоре f выполняется p ∤ g(a)(f(a)), то p не делит произведение f.prod g.

LaTeX

$$pp : Prime p → (∀ a ∈ f.support, ¬p ∣ g a (f a)) → ¬p ∣ f.prod g$$

Lean4

theorem not_dvd_finsuppProd {f : M₀ →₀ M} {g : M₀ → M → ℕ} {p : ℕ} (pp : Prime p)
    (hS : ∀ a ∈ f.support, ¬p ∣ g a (f a)) : ¬p ∣ f.prod g :=
  Prime.not_dvd_finset_prod pp hS

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