dvd_finset_prod_iff — Mathlib

English

If a prime p does not divide any g(a) for a ∈ S, then p does not divide the product ∏ a∈S g(a).

Русский

Если простое p не делит ни одного значения g(a) для a ∈ S, то p не делит произведение ∏_{a∈S} g(a).

LaTeX

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

Lean4

theorem dvd_finset_prod_iff {S : Finset M₀} {p : M} (pp : Prime p) (g : M₀ → M) : p ∣ S.prod g ↔ ∃ a ∈ S, p ∣ g a :=
  ⟨pp.exists_mem_finset_dvd, fun ⟨_, ha1, ha2⟩ => dvd_trans ha2 (dvd_prod_of_mem g ha1)⟩

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