not_dvd_finset_prod — Mathlib

English

For a finite set S and a map g, p divides the product over S of g iff there exists a ∈ S with p ∣ g(a).

Русский

Для конечного множества S и отображения g, p делит произведение ∏ g(a) по S тогда и только тогда существует a ∈ S такое, что p ∣ g(a).

LaTeX

$$pp : Prime p → ∀ {S : Finset M₀} {g : M₀ → M}, p ∣ S.prod g ↔ ∃ a ∈ S, p ∣ g a$$

Lean4

theorem not_dvd_finset_prod {S : Finset M₀} {p : M} (pp : Prime p) {g : M₀ → M} (hS : ∀ a ∈ S, ¬p ∣ g a) :
    ¬p ∣ S.prod g := by exact mt (Prime.dvd_finset_prod_iff pp _).1 <| not_exists.2 fun a => not_and.2 (hS a)

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