coe_zero' — Mathlib

English

The zero map, viewed as a ContinuousAddMonoidHom, is equal to zero in that additive monoid structure.

Русский

Нулевое отображение, рассмотренное как ContinuousAddMonoidHom, равно нулю в соответствующей аддитивной монадной структуре.

LaTeX

$$$ \big( (0 : M_1 \to SL[\sigma_{12}] M_2) \big) \, : ContinuousAddMonoidHom M_1 M_2 = 0. $$$

Lean4

@[norm_cast]
theorem coe_zero' : ⇑(0 : M₁ →SL[σ₁₂] M₂) = 0 :=
  rfl

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