coe_smul — Mathlib

English

The coercion to a linear map commutes with scalar multiplication: ↑(c • f) = c • (f : M1 →ₛₗ[σ12] M2).

Русский

Приведение к линейному отображению сохраняет скалярное умножение: ↑(c • f) = c • (f : M1 →ₛₗ[σ12] M2).

LaTeX

$$$ \uparrow(c \cdot f) = c \cdot (f : M_1 \to_{{\sigma_{12}}} M_2). $$$

Lean4

@[simp, norm_cast]
theorem coe_smul (c : S₂) (f : M₁ →SL[σ₁₂] M₂) : ↑(c • f) = c • (f : M₁ →ₛₗ[σ₁₂] M₂) :=
  rfl

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