map_smul_of_tower — Mathlib

English

For F with LinearMapClass, if compatible smuls hold, then fₗ respects c • x mapping to c • fₗ x.

Русский

Для F с LinearMapClass, при условии совместимых скаляров, fₗ сохраняет умножение скаляров: fₗ (c • x) = c • fₗ x.

LaTeX

$$$ f_\ell (c \cdot x) = c \cdot f_\ell x $$$

Lean4

theorem _root_.LinearMapClass.map_smul_of_tower {F : Type*} [CompatibleSMul M M₂ R S] [FunLike F M M₂]
    [LinearMapClass F S M M₂] (fₗ : F) (c : R) (x : M) : fₗ (c • x) = c • fₗ x :=
  LinearMap.CompatibleSMul.map_smul (fₗ : M →ₗ[S] M₂) c x

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