pow_sup_eq_top — Mathlib

English

Let R be a commutative semiring and I, J be ideals with I + J = ⊤. Then for every n, I^n + J = ⊤.

Русский

Пусть R — коммутативное полукольцо, I и J — идеалы, удовлетворяющие I + J = ⊤. Тогда для каждого n выполняется I^n + J = ⊤.

LaTeX

$$$$ I \sqcup J = \top \Rightarrow \forall n \in \mathbb{N},\ I^n \sqcup J = \top $$$$

Lean4

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

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