zsmul_hom

Mathlib.CategoryTheory.Idempotents.Karoubi

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Idempotents.Karoubi.zsmul_hom

English

The additive action commutes with Karoubi morphisms: (n • f).f = n • f.f for any integer n.

Русский

Сложение на Морфизма Кароуоби совместимо с умножением на целые: (n • f).f = n • f.f.

LaTeX

$$$\text{(n • f).f} = n \cdot (f.f)$$$

Lean4

@[simp]
theorem zsmul_hom [Preadditive C] {P Q : Karoubi C} (n : ℤ) (f : P ⟶ Q) : (n • f).f = n • f.f :=
  map_zsmul (inclusionHom P Q) n f

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

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

Разделы

Аффилиация

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