English
Let M be an additive zero-sorted structure and N an additive monoid. The collection of additive group homomorphisms from M to N carries a natural action of the natural numbers: for a ∈ ℕ and f: M →+ N, define (a · f)(m) = a · f(m). This action respects addition and maps, making Hom_add(M,N) into a ℕ-module.
Русский
Пусть M — аддитивная структура, а N — аддитивный моноид. Множество гомоморфизмов аддитивной группы M в N естественно под действием ℕ: для a ∈ ℕ и f: M →+ N задаётся (a · f)(m) = a · f(m). Это действие сохраняет сложение и отображения, образуя ℕ-модуль Hom_add(M,N).
LaTeX
$$$\text{There is a natural } \mathbb{N}\text{-module structure on }\mathrm{Hom}_{\text{Add}}(M,N)\text{ given by }(a\cdot f)(m)=a\cdot f(m).$$$
Lean4
instance instNatSMul [AddZeroClass M] [AddCommMonoid N] : SMul ℕ (M →+ N) where
smul a
f :=
{ toFun := a • f
map_zero' := by simp
map_add' x y := by simp [nsmul_add] }
