instRepr

Mathlib.NumberTheory.Zsqrtd.GaussianInt

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

English

The embedding is given by mapping a+bi to a+bi in C, i.e., (a+bi) ↦ a+bi.

Русский

Встраивание задается отображением a+bi ↦ a+bi в C.

LaTeX

$$$\\forall a,b\\in\\mathbb{Z},\\; (a+bi) \\mapsto a+bi \\in \\mathbb{C}$.$$

Lean4

instance : Repr ℤ[i] :=
  ⟨fun x _ => "⟨" ++ repr x.re ++ ", " ++ repr x.im ++ "⟩"⟩

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

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

Разделы

Аффилиация

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