add_tensor — Mathlib

English

Let C be a monoidal preadditive category and W,X,Y,Z objects in C. For morphisms f,g: W → X and h: Y → Z, the tensor product distributes over addition on the left: (f + g) ⊗ h = f ⊗ h + g ⊗ h.

Русский

Пусть C — моноидальная предадитивная категория, и возьмём объекты W,X,Y,Z в C. Для отображений f,g: W → X и h: Y → Z выполняется левая дистрибутивность тензорирования: (f + g) ⊗ h = f ⊗ h + g ⊗ h.

LaTeX

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

Lean4

theorem add_tensor {W X Y Z : C} (f g : W ⟶ X) (h : Y ⟶ Z) : (f + g) ⊗ₘ h = f ⊗ₘ h + g ⊗ₘ h := by simp [tensorHom_def]

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