coe_natCast

Mathlib.Algebra.DirectSum.Internal

URI: https://scilib.ai/kg/mathlib#SetLike.GradeZero.coe_natCast

English

Natural numbers embed into A_0 via the GradeZero subsemiring, preserving nat cast.

Русский

Естественные числа встроены в A_0 через GradeZero, сохраняются отображения приведения поNat.

LaTeX

$$$$ (n:\mathbb{N}) : (n:A_0) = (n:R). $$$$

Lean4

@[simp, norm_cast]
theorem coe_natCast (n : ℕ) : (n : A 0) = (n : R) :=
  rfl

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

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

Разделы

Аффилиация

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