instPreadditive

Mathlib.CategoryTheory.Preadditive.Mat

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Mat.instPreadditive

English

For f : M ⟶ N and g : N ⟶ K, the (i,k)-entry of f ≫ g equals ∑ j f_{i j} g_{j k}.

Русский

Для f : M ⟶ N и g : N ⟶ K элемент (i,k) композиции f ≫ g равен сумме ∑_j f_{i j} g_{j k}.

LaTeX

$$$ (f \gg g)_{ik} = \sum_j f_{i j} g_{j k}$$$

Lean4

instance : Preadditive (Mat R) where
  -- TODO show `Mat R` has biproducts, and that `biprod.map` "is" forming a block diagonal matrix.

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

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

Разделы

Аффилиация

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