toComplex_zero

Mathlib.NumberTheory.Zsqrtd.GaussianInt

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

English

The zero Gaussian integer maps to zero in the complex numbers.

Русский

Ноль гауссовых целых отображается в ноль комплексных чисел.

LaTeX

$$$((0:\\mathbb{Z}[i]) : \\mathbb{C}) = 0$.$$

Lean4

theorem toComplex_zero : ((0 : ℤ[i]) : ℂ) = 0 :=
  toComplex.map_zero

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

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

Разделы

Аффилиация

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