instHasBinaryBiproducts

Mathlib.Algebra.Category.Grp.Biproducts

URI: https://scilib.ai/kg/mathlib#AddCommGrpCat.instHasBinaryBiproducts

English

In AddCommGrpCat, the biproduct of G and H is isomorphic to their cartesian product as additive groups.

Русский

В AddCommGrpCat бипродукт G ⊞ H изоморфен их прямому произведению G × H как аддитивные группы.

LaTeX

$$(G ⊞ H) ≅ AddCommGrpCat.of (G × H)$$

Lean4

instance : HasBinaryBiproducts AddCommGrpCat :=
  HasBinaryBiproducts.of_hasBinaryProducts

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

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

Разделы

Аффилиация

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