GaussianInt

Mathlib.NumberTheory.Zsqrtd.GaussianInt

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

English

The Gaussian integers embed into the complex numbers as a ring homomorphism.

Русский

Гауссовы целые числа внедряются в комплексные как кольцевой гомоморфизм.

LaTeX

$$$\\text{toComplex}: \\mathbb{Z}[i] \\to^+_* \\mathbb{C} \\text{ is a ring homomorphism.}$$$

Lean4

/-- The Gaussian integers, defined as `ℤ√(-1)`. -/
abbrev GaussianInt : Type :=
  Zsqrtd (-1)

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

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

Разделы

Аффилиация

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