English
Let AddCommGroup M and M₂, modules over ℚ, F: Type* → M → M₂, with AddMonoidHomClass, then for c ∈ ℚ and x ∈ M, f(c • x) = c • f(x).
Русский
Пусть M и M₂ — AddCommGroup, существуют модули над ℚ, F: Type* → M → M₂, и т.д.; тогда для c ∈ ℚ и x ∈ M выполняется f(c • x) = c • f(x).
LaTeX
$$$f(c \\cdot x) = c \\cdot f(x)\\quad (c \\in \\mathbb{Q}, x \\in M)$$$
Lean4
theorem map_rat_smul [AddCommGroup M] [AddCommGroup M₂] [_instM : Module ℚ M] [_instM₂ : Module ℚ M₂] {F : Type*}
[FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (c : ℚ) (x : M) : f (c • x) = c • f x :=
map_ratCast_smul f ℚ ℚ c x