dvd_finsuppProd_iff — Mathlib

English

For finsupp f and g, p divides f.prod g iff there exists a ∈ support(f) with p ∣ g a (f a).

Русский

Для финсапп f и g, p делит f.prod g тогда и только тогда существует a из поддержки f, такое что p ∣ g a (f a).

LaTeX

$$pp : Prime p → ∀ {f : M₀ →₀ M} {g : M₀ → M → ℕ}, p ∣ f.prod g ↔ ∃ a ∈ f.support, p ∣ g a (f a)$$

Lean4

theorem dvd_finsuppProd_iff {f : M₀ →₀ M} {g : M₀ → M → ℕ} {p : ℕ} (pp : Prime p) :
    p ∣ f.prod g ↔ ∃ a ∈ f.support, p ∣ g a (f a) :=
  Prime.dvd_finset_prod_iff pp _

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