hom_nsmul — Mathlib

English

The action of natural numbers on morphisms in AddCommGrpCat is compatible with the underlying abelian group structure: (n • f).hom = n • f.hom.

Русский

Действие натуральных чисел на морфизмы в AddCommGrpCat согласовано с абелевой структурой: (n • f).hom = n • f.hom.

LaTeX

$$$ (n \cdot f).\mathrm{hom} = n \cdot f.\mathrm{hom} $$$

Lean4

@[simp]
theorem hom_nsmul (n : ℕ) (f : M ⟶ N) : (n • f).hom = n • f.hom :=
  rfl

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