im_toComplex

Mathlib.NumberTheory.Zsqrtd.GaussianInt

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

English

For a Gaussian integer x = a + bi, the imaginary part of its complex image equals b.

Русский

Для x = a + bi мнимая часть изображения в комплекс равна b.

LaTeX

$$@[simp] theorem im_toComplex (x y : ℤ) : ((⟨x, y⟩ : ℤ[i]) : ℂ).im = y := by simp [toComplex_def]$$

Lean4

@[simp]
theorem im_toComplex (x y : ℤ) : ((⟨x, y⟩ : ℤ[i]) : ℂ).im = y := by simp [toComplex_def]

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

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

Разделы

Аффилиация

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