im_mul

Mathlib.NumberTheory.Zsqrtd.Basic

URI: https://scilib.ai/kg/mathlib#Zsqrtd.im_mul

English

The imaginary part of a product satisfies: Im(z w) = Re(z) Im(w) + Im(z) Re(w).

Русский

Мнимая часть произведения удовлетворяет: Im(z w) = Re(z) Im(w) + Im(z) Re(w).

LaTeX

$$$\\Im(z w) = \\Re(z)\\Im(w) + \\Im(z)\\Re(w).$$$

Lean4

@[simp]
theorem im_mul (z w : ℤ√d) : (z * w).im = z.re * w.im + z.im * w.re :=
  rfl

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

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

Разделы

Аффилиация

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