sup_multiset_prod_eq_top — Mathlib

English

Let I be an ideal and s a multiset of ideals. If for every p in s we have I ⊔ p = ⊤, then I ⊔ s.prod = ⊤.

Русский

Пусть I — идеал, а s — мультсет идеалов. Если для каждого p ∈ s выполняется I ⊔ p = ⊤, тогда I ⊔ s.prod = ⊤.

LaTeX

$$$ I \oplus \operatorname{prod} s = \top \quad \text{if } \forall p \in s, I \oplus p = \top. $$$

Lean4

theorem sup_multiset_prod_eq_top {s : Multiset (Ideal R)} (h : ∀ p ∈ s, I ⊔ p = ⊤) : I ⊔ Multiset.prod s = ⊤ :=
  Multiset.prod_induction (I ⊔ · = ⊤) s (fun _ _ hp hq ↦ (sup_mul_eq_of_coprime_left hp).trans hq)
    (by simp only [one_eq_top, le_top, sup_of_le_right]) h

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