tensorObj_eq

Mathlib.Algebra.Category.Grp.CartesianMonoidal

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

English

The tensor product in CommGrpCat equals the cartesian product of underlying groups.

Русский

Тензорное произведение CommGrpCat эквивалентно прямому произведению базовых групп.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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