toComplex_mul

Mathlib.NumberTheory.Zsqrtd.GaussianInt

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

English

The complex embedding preserves multiplication on Gaussian integers.

Русский

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

LaTeX

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

Lean4

theorem toComplex_mul (x y : ℤ[i]) : ((x * y : ℤ[i]) : ℂ) = x * y :=
  toComplex.map_mul _ _

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

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

Разделы

Аффилиация

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