map_smul — Mathlib

English

A map that is linear with respect to the action commutes with smul: f(c•x) = c•f(x).

Русский

Линейное отображение по отношению к действию коммутирует с умножением: f(c•x) = c•f(x).

LaTeX

$$$f(c\\cdot x) = c\\cdot f(x) \\quad(\\text{for all } c\\in M, x\\in X)$$$

Lean4

@[to_additive (attr := simp)]
theorem map_smul {F M X Y : Type*} [SMul M X] [SMul M Y] [FunLike F X Y] [MulActionHomClass F M X Y] (f : F) (c : M)
    (x : X) : f (c • x) = c • f x :=
  map_smulₛₗ f c x

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