exists_mem_finset_dvd — Mathlib

English

Let p be prime in M₀. For any finite set s ⊆ ι with function f: ι → M₀, if p divides the product over s, then there exists i ∈ s with p ∣ f(i).

Русский

Пусть p — простое в M₀. Для любого конечного множества s ⊆ ι с функцией f: ι → M₀, если p делит произведение по s, тогда существует i ∈ s такое, что p делит f(i).

LaTeX

$$hp : Prime p → ∀ {s : Finset ι} {f : ι → M₀}, p ∣ (s.prod f) → ∃ i ∈ s, p ∣ f i$$

Lean4

theorem exists_mem_finset_dvd (hp : Prime p) {s : Finset ι} {f : ι → M₀} : p ∣ s.prod f → ∃ i ∈ s, p ∣ f i :=
  hp.exists_mem_multiset_map_dvd

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