map_smul_of_tower — Mathlib

English

For any f in ContinuousLinearMap, its underlying semilinear map equals f when viewed as a map.

Русский

Для любого f из ContinuousLinearMap базовая семилинейная карта совпадает с f как отображение.

LaTeX

$$f :SL[σ12] M1 M2$$

Lean4

@[simp]
theorem map_smul_of_tower {R S : Type*} [Semiring S] [SMul R M₁] [Module S M₁] [SMul R M₂] [Module S M₂]
    [LinearMap.CompatibleSMul M₁ M₂ R S] (f : M₁ →L[S] M₂) (c : R) (x : M₁) : f (c • x) = c • f x :=
  LinearMap.CompatibleSMul.map_smul (f : M₁ →ₗ[S] M₂) c x

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