coe_zero — Mathlib

English

The linear-coercion of the zero map equals the zero linear map: ((0) : M1 →SL[σ12] M2) = 0 in the appropriate semilinear map space.

Русский

Коэрцирование нулевого отображения равно нулю в пространстве полулинейных отображений.

LaTeX

$$$ \Big((0 : M_1 \to SL[\sigma_{12}] M_2) : M_1 \to_{\sigma_{12}} M_2\Big) = 0. $$$

Lean4

@[simp, norm_cast]
theorem coe_zero : ((0 : M₁ →SL[σ₁₂] M₂) : M₁ →ₛₗ[σ₁₂] M₂) = 0 :=
  rfl

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