top_prod_top

Mathlib.Algebra.Ring.Subsemiring.Basic

URI: https://scilib.ai/kg/mathlib#Subsemiring.top_prod_top

English

The product of top subsemirings equals the top: (⊤: Subsemiring R).prod (⊤: Subsemiring S) = ⊤.

Русский

Произведение верхних подполу: (⊤: Subsemiring R).prod (⊤: Subsemiring S) = ⊤.

LaTeX

$$$(\\top : Subsemiring R).prod(\\top : Subsemiring S) = \\top$$$

Lean4

@[simp]
theorem top_prod_top : (⊤ : Subsemiring R).prod (⊤ : Subsemiring S) = ⊤ :=
  (top_prod _).trans <| comap_top _

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

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

Разделы

Аффилиация

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