English
If f is a map between AddCommMonoid modules that is FunLike and AddMonoidHomClass, then for x ∈ ℤ and a ∈ M, f((x : R) • a) = (x : S) • f a.
Русский
Если f — отображение между модулями с формой FunLike и AddMonoidHomClass, то для x ∈ ℤ и a ∈ M выполняется f((x : R) • a) = (x : 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_intCast_smul [AddCommGroup M] [AddCommGroup M₂] {F : Type*} [FunLike F M M₂] [AddMonoidHomClass F M M₂]
(f : F) (R S : Type*) [Ring R] [Ring S] [Module R M] [Module S M₂] (x : ℤ) (a : M) :
f ((x : R) • a) = (x : S) • f a := by simp only [Int.cast_smul_eq_zsmul, map_zsmul]
