prod_bot_bot

Mathlib.RingTheory.Ideal.Prod

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

English

In the product ring R × S, the product of the bottom ideals is the bottom ideal of R × S.

Русский

В произведении колец R × S произведение нулевых идеалов равно нулевому идеалу в R × S.

LaTeX

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

Lean4

@[simp]
theorem prod_bot_bot : prod (⊥ : Ideal R) (⊥ : Ideal S) = ⊥ :=
  SetLike.coe_injective <| Set.singleton_prod_singleton

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

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

Разделы

Аффилиация

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