coe_zero

Mathlib.Data.ENat.Basic

URI: https://scilib.ai/kg/mathlib#ENat.coe_zero

English

The natural embedding of 0 into ENNat yields 0.

Русский

Встраивание 0 в ENat дает 0.

LaTeX

$$$$ (0 : \\mathbb{N}_{\\infty}) = 0. $$$$

Lean4

theorem coe_zero : ((0 : ℕ) : ℕ∞) = 0 :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru