comp_as_mul

Mathlib.CategoryTheory.SingleObj

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SingleObj.comp_as_mul

English

In the single-object category, composition corresponds to multiplication: f ≫ g = g f.

Русский

В однообъектной категории композиция соответствует умножению: f ≫ g = g f.

LaTeX

$$$ f \;\circ\; g = g f. $$$

Lean4

theorem comp_as_mul {x y z : SingleObj M} (f : x ⟶ y) (g : y ⟶ z) : f ≫ g = g * f :=
  rfl

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

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

Разделы

Аффилиация

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