of_intCast

Mathlib.Data.Num.ZNum

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

English

Embedding is injective: (m : α) = (n : α) iff m = n.

Русский

Встраивание инъективно: (m : α) = (n : α) iff m = n.

LaTeX

$$$$\forall {m,n : ZNum},\ (m : \alpha) = (n : \alpha) \iff m = n.$$$$

Lean4

@[simp, norm_cast]
theorem of_intCast [AddGroupWithOne α] (n : ℤ) : ((n : ZNum) : α) = n := by rw [← cast_to_int, to_of_int]

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

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

Разделы

Аффилиация

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