prod_top_top

Mathlib.RingTheory.Ideal.Prod

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

English

In the product of semirings R × S, the product of the top ideals from R and S is the top ideal of R × S.

Русский

В произведении колец R × S произведение верхних идеалов R и S есть верхний идеал в R × S.

LaTeX

$$$\\operatorname{prod}(\\top, \\top) = \\top$$$

Lean4

@[simp]
theorem prod_top_top : prod (⊤ : Ideal R) (⊤ : Ideal S) = ⊤ :=
  Ideal.ext <| by simp

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

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

Разделы

Аффилиация

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