hom_ext

Mathlib.CategoryTheory.Preadditive.Mat

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Mat_.hom_ext

English

The associativity of composition in Mat_ C follows by standard finite sums over intermediate indices.

Русский

Ассоциативность композиции в Mat_ C следует из стандартной суммы по промежуточным индексам.

LaTeX

$$$comp\_def {M N K} (f) (g) = ...$$$

Lean4

@[ext]
theorem hom_ext {M N : Mat_ C} (f g : M ⟶ N) (H : ∀ i j, f i j = g i j) : f = g :=
  DMatrix.ext_iff.mp H

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

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

Разделы

Аффилиация

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