tensor_add

Mathlib.CategoryTheory.Monoidal.Preadditive

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

English

Repeatedly same as Tensor Add: 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

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

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

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

Разделы

Аффилиация

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