intCast_injective

Mathlib.Data.Rat.Defs

URI: https://scilib.ai/kg/mathlib#Rat.intCast_injective

English

The map Int.cast from integers to rationals is injective: if Int.cast a = Int.cast b then a = b.

Русский

Отображение Int.cast из целых чисел в рациональные безошибочно инъективно: если Int.cast a = Int.cast b, то a = b.

LaTeX

$$Injective(Int.cast : Z → Q)$$

Lean4

theorem intCast_injective : Injective (Int.cast : ℤ → ℚ) := fun _ _ ↦ congr_arg num

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

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

Разделы

Аффилиация

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