to_int_inj

Mathlib.Data.Num.ZNum

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

English

For every integer n, casting to ZNum and back to ℤ returns the original integer.

Русский

Для каждого целого числа n отображение в ZNum и обратное возвращают исходное число.

LaTeX

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

Lean4

theorem to_int_inj {m n : ZNum} : (m : ℤ) = n ↔ m = n :=
  ⟨fun h => Function.LeftInverse.injective of_to_int' h, congr_arg _⟩

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

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

Разделы

Аффилиация

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