coe_zero — Mathlib

English

The identity and zero maps behave as expected in the morphism structure: coe(0) = 0 and coe(1) = id.

Русский

Идентичная и нулевая карты ведут себя как положено: отображение 0 — ноль, отображение 1 — тождественное отображение.

LaTeX

$$$ \\text{coe\_zero} : (0 : A \\to_{e+[\\phi]} B)(a) = 0 \\\\ $ and \\\\ $ \\text{coe\_one} : (1 : A \\to_{e+[\\phi]} A) = \\mathrm{id}_A $$$

Lean4

@[simp]
theorem coe_zero : ⇑(0 : A →ₑ+[φ] B) = 0 :=
  rfl

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