map_smul_of_tower — Mathlib

English

A positive linear map commutes with tower scalar multiplication: f(c • x) = c • f(x).

Русский

Положительное линейное отображение сохраняет умножение на внешние скаляры: f(c • x) = c • f(x).

LaTeX

$$$f(c\\cdot x) = c\\cdot f(x)$$$

Lean4

@[simp]
theorem map_smul_of_tower {S : Type*} [SMul S E₁] [SMul S E₂] [LinearMap.CompatibleSMul E₁ E₂ S R] (f : E₁ →ₚ[R] E₂)
    (c : S) (x : E₁) : f (c • x) = c • f x :=
  LinearMapClass.map_smul_of_tower f _
    _
      -- We add the more specific lemma here purely for the aesop tag.

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