English
In a commutative ring, with a finite index set and two distinguished indices a, b, if all other f(i) are prime, then I ⊆ ⋃ f(i) implies I ⊆ f(a) or I ⊆ f(b) or I ⊆ f(i) for some i ∈ s.
Русский
В коммутативном кольце, для конечного множества индексов, и двух выделенных индексов a, b, если все прочие f(i) простые, то если I ⊆ ⋃ f(i), то либо I ⊆ f(a), либо I ⊆ f(b), либо существует i ∈ s, I ⊆ f(i).
LaTeX
$$$\forall a,b,\ if\ hp: \forall i \in s, i \neq a, i \neq b \Rightarrow IsPrime (f i)\,:\n (I \subseteq f a \cup f b \cup \bigcup_{i\in s} f i) \Rightarrow (I \subseteq f a) \lor (I \subseteq f b) \lor \exists i \in s, I \subseteq f i $$$
Lean4
/-- The product of a finite number of elements in the commutative semiring `R` lies in the
prime ideal `p` if and only if at least one of those elements is in `p`. -/
theorem prod_mem_iff {s : Finset ι} {x : ι → R} {p : Ideal R} [hp : p.IsPrime] : ∏ i ∈ s, x i ∈ p ↔ ∃ i ∈ s, x i ∈ p :=
by
simp_rw [← span_singleton_le_iff_mem, ← prod_span_singleton]
exact hp.prod_le
