multiset_prod_map_le — Mathlib

English

For a prime P and a function f from an index set to ideals, the product of the image of f over a multiset s is ≤ P if and only if there exists an i in s with f(i) ≤ P.

Русский

Для простого P и функции f от индексов к идеалам, произведение образа f по мультимножеству s ≤ P тогда существует i ∈ s, такой что f(i) ≤ P.

LaTeX

$$$ P.IsPrime \Rightarrow (s.map f).prod \le P \iff \exists i \in s, f i \le P $$$

Lean4

theorem multiset_prod_map_le {s : Multiset ι} (f : ι → Ideal R) {P : Ideal R} (hp : IsPrime P) :
    (s.map f).prod ≤ P ↔ ∃ i ∈ s, f i ≤ P := by
  simp_rw [hp.multiset_prod_le, Multiset.mem_map, exists_exists_and_eq_and]

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