instIntCast

Mathlib.Data.Complex.Basic

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

English

There is a canonical embedding of the natural numbers into the complex numbers sending n to n.

Русский

Существует каноническое вложение натуральных чисел в комплексные числа, переводящее n в n.

LaTeX

$$$\\operatorname{natCast}(n) = n$$$

Lean4

instance instIntCast : IntCast ℂ where intCast n := ofReal n

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

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

Разделы

Аффилиация

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