top_prod_top

Mathlib.Algebra.Ring.Subring.Basic

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

English

Product of subrings is isomorphic to their product as rings: prodEquiv (s) (t) : s.prod t ≃+* s × t.

Русский

Произведение подкольц изоморфно их произведению как кольца: prodEquiv(s)(t) : s.prod t ≃+* s × t.

LaTeX

$$$ \mathrm{prodEquiv}(s,t) : s.prod t \cong+* s \times t $$$

Lean4

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

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

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

Разделы

Аффилиация

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