app_nsmul — Mathlib

English

The action of an integer scalar on natural-numbered morphisms is compatible pointwise on components; the component map respects zsmul.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem app_nsmul (X : C) (α : F ⟶ G) (n : ℕ) : (n • α).app X = n • α.app X :=
  (appHom X).map_nsmul α n

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