zero_tensor

Mathlib.CategoryTheory.Monoidal.Preadditive

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MonoidalPreadditive.zero_tensor

English

In a monoidal preadditive category, tensoring with zero on the left yields zero: (0) ⊗_m f = 0.

Русский

В моноидальной предаддитивной категории тензорирование с нулём слева даёт ноль: 0 ⊗_m f = 0.

LaTeX

$$$$ (0 : W \\to X) \\otimes_m f = 0 $$$$

Lean4

@[simp (low)]
theorem zero_tensor {W X Y Z : C} (f : Y ⟶ Z) : (0 : W ⟶ X) ⊗ₘ f = 0 := by simp [tensorHom_def]

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

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

Разделы

Аффилиация

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