cast_injective

Mathlib.Data.Int.Cast.Lemmas

URI: https://scilib.ai/kg/mathlib#Int.cast_injective

English

Injectivity of the integer cast: m.cast = n.cast implies m = n.

Русский

Инъективность приведения целых: если m.cast = n.cast, то m = n.

LaTeX

$$$ \forall {\alpha} [AddGroupWithOne \alpha] [CharZero \alpha],\ (m,n : \mathbb{Z}),\ Inequation( (m : \alpha), (n : \alpha) ).$$

Lean4

theorem cast_injective : Injective (Int.cast : ℤ → α) := fun _ _ ↦ cast_inj.1

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

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

Разделы

Аффилиация

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