map_smul — Mathlib

English

The constructed object, when viewed as a DistribMulActionHom, coincides with the underlying function view of f.

Русский

Сконструированный объект, рассматриваемый как DistribMulActionHom, совпадает с представлением f как функции.

LaTeX

$$$((\langle f,h_1,h_2,h_3,h_4\rangle : A \to_{\varphi} B) : A \to_{e+[\varphi]} B) = \langle f,h_1\rangle$$$

Lean4

@[simp] -- Marked as `@[simp]` because `MulActionSemiHomClass.map_smulₛₗ` can't be.

protected theorem map_smul (f : A →ₛₙₐ[φ] B) (c : R) (x : A) : f (c • x) = (φ c) • f x :=
  map_smulₛₗ _ _ _

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