prod_le — Mathlib

English

Let P be prime. For a finite set s and a family of ideals f(i), the product over s is ≤ P iff there exists i ∈ s with f(i) ≤ P.

Русский

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

LaTeX

$$∀ {s : Finset ι} {f : ι → Ideal R} {P : Ideal R}, P.IsPrime → (s.prod f ≤ P) ↔ ∃ i ∈ s, f i ≤ P$$

Lean4

theorem prod_le {s : Finset ι} {f : ι → Ideal R} {P : Ideal R} (hp : IsPrime P) : s.prod f ≤ P ↔ ∃ i ∈ s, f i ≤ P :=
  hp.multiset_prod_map_le f

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