map_smul — Mathlib

English

The map operation commutes with scalar multiplication: (r • x).map f = r • (x.map f) for a linear map f.

Русский

Операция отображения commute со скалярным умножением: (r • x).map f = r • (x.map f) при линейном отображении f.

LaTeX

$$$(r \\cdot x).map f = r \\cdot (x.map f)$$$

Lean4

@[simp]
protected theorem map_smul [AddCommMonoid U] [Module R U] (f : U →ₗ[R] V) {r : R} {x : HahnSeries Γ U} :
    (r • x).map f = r • ((x.map f) : HahnSeries Γ V) := by ext; simp

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