toComplex_add

Mathlib.NumberTheory.Zsqrtd.GaussianInt

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

English

The complex embedding preserves addition on Gaussian integers.

Русский

Гомоморфизм в комплекс сохраняет сложение на гауссовых целых.

LaTeX

$$$\\forall x,y\\in \\mathbb{Z}[i],\\; ((x+y:\\mathbb{Z}[i]):\\mathbb{C}) = x+y$.$$

Lean4

theorem toComplex_add (x y : ℤ[i]) : ((x + y : ℤ[i]) : ℂ) = x + y :=
  toComplex.map_add _ _

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

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

Разделы

Аффилиация

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