toComplex_neg

Mathlib.NumberTheory.Zsqrtd.GaussianInt

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

English

The complex embedding respects negation: toComplex(-x) = -toComplex(x).

Русский

Гомоморфизм сохраняет отрицание: toComplex(-x) = -toComplex(x).

LaTeX

$$$\\forall x\\in \\mathbb{Z}[i],\\; \\text{toComplex}(-x) = -\\text{toComplex}(x).$$$

Lean4

theorem toComplex_neg (x : ℤ[i]) : ((-x : ℤ[i]) : ℂ) = -x :=
  toComplex.map_neg _

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

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

Разделы

Аффилиация

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