coe_toNatHom

Mathlib.Data.ENat.Basic

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

English

The coercion-based functor equality: coe ENat.toNatHom = toNatHom, i.e., the canonical embedding agrees with the explicit hom.

Русский

Согласование канонического вложения и явного гомоморфизма: coe ENat.toNatHom = toNatHom.

LaTeX

$$$\\\\mathrm{coe} (\\\\operatorname{ENat.toNatHom}) = \\\\operatorname{toNatHom}.$$$

Lean4

@[simp, norm_cast]
theorem coe_toNatHom : toNatHom = toNat :=
  rfl

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

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

Разделы

Аффилиация

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