exists_mem_multiset_map_dvd — Mathlib

English

Let p be prime in M₀ and s a multiset with index set ι and f: ι → M₀. If p divides the product of the mapped multiset, (s.map f).prod, then there exists a ∈ s such that p ∣ f(a).

Русский

Пусть p — простое в M₀ и s — мультимножество с отображением f: ι → M₀. Если p делит произведение отображённого мультисета, то существует a ∈ s такое, что p делит f(a).

LaTeX

$$$p$ is prime in $M_0$ and $s$ is a multiset with map $f$. If $p \\mid (s.map\\, f).prod$, then $\\exists a \\in s$ with $p \\mid f(a)$.$$

Lean4

theorem exists_mem_multiset_map_dvd (hp : Prime p) {s : Multiset ι} {f : ι → M₀} :
    p ∣ (s.map f).prod → ∃ a ∈ s, p ∣ f a := fun h => by
  simpa only [exists_prop, Multiset.mem_map, exists_exists_and_eq_and] using hp.exists_mem_multiset_dvd h

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