multiset_prod_le — Mathlib

English

Let P be prime. For any finite collection of ideals I_i, the product ∏ I_i ≤ P if and only if some I_i ≤ P.

Русский

Пусть P прост. Для конечного набора идеалов I_i верно ∏ I_i ≤ P тогда и только если какой-либо I_i ≤ P.

LaTeX

$$$ P.IsPrime \Rightarrow (\prod_{i \in s} I_i \le P) \iff \exists i \in s, I_i \le P $$$

Lean4

theorem multiset_prod_le {s : Multiset (Ideal R)} {P : Ideal R} (hp : IsPrime P) : s.prod ≤ P ↔ ∃ I ∈ s, I ≤ P :=
  s.induction_on (by simp [hp.ne_top]) fun I s ih ↦ by simp [hp.mul_le, ih]

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