intCast_im

Mathlib.NumberTheory.Zsqrtd.GaussianInt

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

English

Kernel of the norm map equals the unitary submonoid.

Русский

Ядро отображения нормы совпадает с подмоноидом единичных элементов.

LaTeX

$$$\\mathrm{mker}(\\text{normMonoidHom})=\\mathrm{unitary}(\\mathbb{Z}[\\sqrt{d}]).$$$

Lean4

@[simp]
theorem intCast_im (x : ℤ[i]) : ((x.im : ℤ) : ℝ) = (x : ℂ).im := by simp [toComplex_def]

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

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

Разделы

Аффилиация

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