to_of_int

Mathlib.Data.Num.ZNum

URI: https://scilib.ai/kg/mathlib#ZNum.to_of_int

English

For any m,n ∈ ZNum, (m : ℤ) = n iff m = n.

Русский

Для любых m,n ∈ ZNum, (m : ℤ) = n эквивалентно m = n.

LaTeX

$$$$\forall {m,n \in ZNum},\ (m : \mathbb{Z}) = n \iff m = n.$$$$

Lean4

theorem to_of_int (n : ℤ) : ((n : ZNum) : ℤ) = n :=
  Int.inductionOn' n 0 (by simp) (by simp) (by simp)

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

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

Разделы

Аффилиация

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