pow_sup_pow_eq_top

Mathlib.RingTheory.Ideal.Operations

URI: https://scilib.ai/kg/mathlib#Ideal.pow_sup_pow_eq_top

English

Let I, J be ideals with I + J = ⊤. Then for all m, n, I^m + J^n = ⊤.

Русский

Пусть I и J — идеалы, удовлетворяющие I + J = ⊤. Тогда для любых m, n выполняется I^m + J^n = ⊤.

LaTeX

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

Lean4

theorem pow_sup_pow_eq_top {m n : ℕ} (h : I ⊔ J = ⊤) : I ^ m ⊔ J ^ n = ⊤ :=
  sup_pow_eq_top (pow_sup_eq_top h)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru