instCoeComplex

Mathlib.NumberTheory.Zsqrtd.GaussianInt

URI: https://scilib.ai/kg/mathlib#GaussianInt.instCoeComplex

English

There is a canonical Coe from ℤ[i] to ℂ, i.e., a default way to view Gaussian integers as complex numbers.

Русский

Существует каноническое приведение из ℤ[i] к ℂ, т.е. способ рассматривать гауссовы целые как комплексные числа по умолчанию.

LaTeX

$$Instance: Coe ℤ[i] ℂ$$

Lean4

instance : Coe ℤ[i] ℂ :=
  ⟨toComplex⟩

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

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

Разделы

Аффилиация

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