English
If f is a linear-like map between modules with a FunLike/AddMonoidHomClass structure, then for any natural n and a ∈ M, f((n : R) • a) = (n : S) • f(a).
Русский
Если f — отображение, совместимое с операциями модуля, между модулями с соответствующими структурами, то для любого натурального n и a ∈ M выполняется f((n : R) • a) = (n : S) • f(a).
LaTeX
$$$\\forall {M} {M_2} [\\! AddCommMonoid M] [\\! AddCommMonoid M_2] \\{F : Type*\\} [FunLike F M M_2] [AddMonoidHomClass F M M_2] (f : F) (R : Type*) (S : Type*) [Semiring R] [Semiring S] [Module R M] [Module S M_2] (x : \\mathbb{N}) (a : M),\\ f ((x : R) • a) = (x : S) • f a$$$
Lean4
theorem map_natCast_smul [AddCommMonoid M] [AddCommMonoid M₂] {F : Type*} [FunLike F M M₂] [AddMonoidHomClass F M M₂]
(f : F) (R S : Type*) [Semiring R] [Semiring S] [Module R M] [Module S M₂] (x : ℕ) (a : M) :
f ((x : R) • a) = (x : S) • f a := by simp only [Nat.cast_smul_eq_nsmul, map_nsmul]
