ofReal_intCast

Mathlib.Data.Complex.Basic

URI: https://scilib.ai/kg/mathlib#Complex.ofReal_intCast

English

There is a canonical embedding of integers into ℂ via intCast n := ofReal n.

Русский

Существует каноническое вложение целых чисел в ℂ через intCast n := ofReal n.

LaTeX

$$$\\operatorname{intCast}(n) = \\operatorname{ofReal}(n)$$$

Lean4

@[simp, norm_cast]
theorem ofReal_intCast (n : ℤ) : ofReal n = n :=
  rfl

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

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

Разделы

Аффилиация

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