coe_zero — Mathlib

English

The coercion of the zero element equals the zero function: the zero compactly supported map corresponds to the zero function.

Русский

Приведение нулевого элемента равно нулевой функции: нулевое компактно поддерживаемое отображение соответствует нулю функции.

LaTeX

$$$ \mathrm{coe}(0) = 0 $$$

Lean4

@[simp]
theorem coe_zero [Zero β] : ⇑(0 : C_c(α, β)) = 0 :=
  rfl

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