toComplex_sub

Mathlib.NumberTheory.Zsqrtd.GaussianInt

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

English

The complex embedding preserves subtraction: toComplex(x-y) = toComplex(x) - toComplex(y).

Русский

Гомоморфизм сохраняет вычитание: toComplex(x−y) = toComplex(x) − toComplex(y).

LaTeX

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

Lean4

theorem toComplex_sub (x y : ℤ[i]) : ((x - y : ℤ[i]) : ℂ) = x - y :=
  toComplex.map_sub _ _

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

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

Разделы

Аффилиация

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