prod_toNonUnitalSubalgebra

Mathlib.Algebra.Star.NonUnitalSubalgebra

URI: https://scilib.ai/kg/mathlib#NonUnitalStarSubalgebra.prod_toNonUnitalSubalgebra

English

Equality of subalgebra structures on the product and their components.

Русский

Равенство структур подпалгебр на произведении и его составляющих.

LaTeX

$$(S.prod S_1).toNonUnitalSubalgebra = S.toNonUnitalSubalgebra.prod S_1.toNonUnitalSubalgebra$$

Lean4

theorem prod_toNonUnitalSubalgebra :
    (S.prod S₁).toNonUnitalSubalgebra = S.toNonUnitalSubalgebra.prod S₁.toNonUnitalSubalgebra :=
  rfl

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

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

Разделы

Аффилиация

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