English
Let h: M₂ →SL[σ₂₃] M₃ be σ₂₃-semi-linear and f: M →SL[σ₁₂] M₂ be σ₁₂-semi-linear. For any c in R₂, the composition after scaling equals the σ₂₃-action on the scalar times the composition: h ∘ (c • f) = σ₂₃(c) • (h ∘ f).
Русский
Пусть h: M₂ →SL[σ₂₃] M₃ и f: M →SL[σ₁₂] M₂ — полулинейные отображения. Тогда для скаляра c из R₂ выполняется: h ∘ (c • f) = σ₂₃(c) • (h ∘ f).
LaTeX
$$$$ h \circ (c \cdot f) = \sigma_{23}(c) \cdot (h \circ f). $$$$
Lean4
@[simp]
theorem comp_smulₛₗ [SMulCommClass R₂ R₂ M₂] [SMulCommClass R₃ R₃ M₃] [ContinuousConstSMul R₂ M₂]
[ContinuousConstSMul R₃ M₃] (h : M₂ →SL[σ₂₃] M₃) (c : R₂) (f : M →SL[σ₁₂] M₂) : h.comp (c • f) = σ₂₃ c • h.comp f :=
by
ext x
simp only [coe_smul', coe_comp', Function.comp_apply, Pi.smul_apply, ContinuousLinearMap.map_smulₛₗ]
