toContinuousAddMonoidHom_zero — Mathlib

English

The scalar action on maps commutes with the coercion to a linear map: ↑(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 toContinuousAddMonoidHom_zero : ((0 : M₁ →SL[σ₁₂] M₂) : ContinuousAddMonoidHom M₁ M₂) = 0 :=
  rfl

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