multiset_prod_mem_iff_exists_mem — Mathlib

English

Let I be a prime ideal and s a multiset of elements of R. Then the product s.prod x ∈ I iff there exists p ∈ s with p ∈ I.

Русский

Пусть I простой идеал и s — мультисет элементов кольца R. Тогда произведение s = ∏ p ∈ s p ∈ I тогда существует p ∈ s с p ∈ I.

LaTeX

$$$ I.IsPrime \Rightarrow (s.prod \in I) \iff \exists p \in s, p \in I $$$

Lean4

theorem multiset_prod_mem_iff_exists_mem {I : Ideal R} (hI : I.IsPrime) (s : Multiset R) :
    s.prod ∈ I ↔ ∃ p ∈ s, p ∈ I := by simpa [span_singleton_le_iff_mem] using (hI.multiset_prod_map_le (span {·}))

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