sup_pow_eq_top — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem sup_pow_eq_top {n : ℕ} (h : I ⊔ J = ⊤) : I ⊔ J ^ n = ⊤ :=
  by
  rw [← Finset.card_range n, ← Finset.prod_const]
  exact sup_prod_eq_top fun _ _ => h

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