ofInt'_toZNum

Mathlib.Data.Num.ZNum

URI: https://scilib.ai/kg/mathlib#Num.ofInt'_toZNum

← MathLib Explorer

English

For natural n, toZNum n = ZNum.ofInt' n.

Русский

Для натурального n: toZNum n = ZNum.ofInt' n.

LaTeX

$$$$\forall n:\mathbb{N},\ \mathrm{toZNum}(n) = \mathrm{ZNum.ofInt'}(n).$$$$

Lean4

theorem ofInt'_toZNum : ∀ n : ℕ, toZNum n = ZNum.ofInt' n
  | 0 => rfl
  | n + 1 => by rw [Nat.cast_succ, Num.add_one, toZNum_succ, ofInt'_toZNum n, Nat.cast_succ, succ_ofInt', ZNum.add_one]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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