tensor_zero — Mathlib

English

In a monoidal preadditive category, tensoring distributes over addition in the second argument: f ⊗_m (g + h) = f ⊗_m g + f ⊗_m h.

Русский

В моноидальной предадитивной категории тензорирование распределяется по сложению во втором аргументе: f ⊗_m (g + h) = f ⊗_m g + f ⊗_m h.

LaTeX

$$$$ f \\otimes_m (g + h) = f \\otimes_m g + f \\otimes_m h $$$$

Lean4

@[simp (low)]
theorem tensor_zero {W X Y Z : C} (f : W ⟶ X) : f ⊗ₘ (0 : Y ⟶ Z) = 0 := by
  simp [tensorHom_def]
    -- The priority setting will not be needed when we replace `f ⊗ₘ 𝟙 X` by `f ▷ X`.

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