mul_im

Mathlib.Data.Complex.Basic

URI: https://scilib.ai/kg/mathlib#Complex.mul_im

English

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

Русский

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

LaTeX

$$$(z w).im = z.re w.im + z.im w.re$$

Lean4

@[simp]
theorem mul_im (z w : ℂ) : (z * w).im = z.re * w.im + z.im * w.re :=
  rfl

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

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

Разделы

Аффилиация

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