tensorObj_eq

Mathlib.Algebra.Category.Grp.CartesianMonoidal

URI: https://scilib.ai/kg/mathlib#AddGrpCat.tensorObj_eq

English

The tensor object in AddCommGrpCat equals the cartesian product of the underlying additive groups.

Русский

Тензорный объект в AddCommGrpCat равен прямому произведению базовых аддитивных групп.

LaTeX

$$$(G \otimes H) = \mathrm{of}(G \times H)$$$

Lean4

theorem tensorObj_eq (G H : AddGrpCat.{u}) : (G ⊗ H) = of (G × H) :=
  rfl

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

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

Разделы

Аффилиация

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