prod_toSubmodule

Mathlib.Algebra.Algebra.Subalgebra.Prod

URI: https://scilib.ai/kg/mathlib#Subalgebra.prod_toSubmodule

English

Top of the product equals the product of the tops.

Русский

Верх произведения равен произведению вершин.

LaTeX

$$prod_top : (prod ⊤ ⊤) = ⊤$$

Lean4

theorem prod_toSubmodule : toSubmodule (S.prod S₁) = (toSubmodule S).prod (toSubmodule S₁) :=
  rfl

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

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

Разделы

Аффилиация

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