add_comp

Mathlib.CategoryTheory.Preadditive.OfBiproducts

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SemiadditiveOfBinaryBiproducts.add_comp

← MathLib Explorer

English

Distributivity of addition over composition: (f + g) ≫ h = f ≫ h + g ≫ h.

Русский

Дистрибутивность сложения над композицией: (f + g) ≫ h = f ≫ h + g ≫ h.

LaTeX

$$$ (f + g) \;\; \gg \; h = f \gg h + g \gg h $$$

Lean4

theorem add_comp (f g : X ⟶ Y) (h : Y ⟶ Z) : (f + g) ≫ h = f ≫ h + g ≫ h :=
  by
  simp only [add_eq_right_addition, Category.assoc]
  congr
  ext <;> simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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