app_zsmul — Mathlib

English

Integer scalar action on natural numbers above is zsmul of morphisms; the component respects zsmul at X.

Русский

Действие целочисленного множителя на компоненты морфизмов соответствует zsmul на уровне компоненты.

LaTeX

$$$$ (n\\cdot\\alpha).\\text{app } X = n\\cdot (\\alpha.\\text{app }X). $$$$

Lean4

@[simp]
theorem app_zsmul (X : C) (α : F ⟶ G) (n : ℤ) : (n • α).app X = n • α.app X :=
  (appHom X : (F ⟶ G) →+ (F.obj X ⟶ G.obj X)).map_zsmul α n

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