map_rat_smul — Mathlib

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

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