comp_smul — Mathlib

English

Let h: N₂ → N₃ be an R-linear continuous map and f: M → N₂ be an R-linear continuous map. For any scalar c from S, the composition after scaling equals scaling of the composition: h ∘ (c · f) = c · (h ∘ f).

Русский

Пусть h: N₂ → N₃ и f: M → N₂ — непрерывные линейные отображения над R. Тогда для произвольного скаляра c из S выполнено: h ∘ (c · f) = c · (h ∘ f).

LaTeX

$$$$ h \circ (c \cdot f) = c \cdot (h \circ f). $$$$

Lean4

@[simp]
theorem comp_smul [LinearMap.CompatibleSMul N₂ N₃ S R] (hₗ : N₂ →L[R] N₃) (c : S) (fₗ : M →L[R] N₂) :
    hₗ.comp (c • fₗ) = c • hₗ.comp fₗ := by
  ext x
  exact hₗ.map_smul_of_tower c (fₗ x)

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