mul_im

Mathlib.Analysis.RCLike.Basic

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

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

$$$\mathrm{im}(z w) = \mathrm{re}(z) \mathrm{im}(w) + \mathrm{im}(z) \mathrm{re}(w)$$$

Lean4

@[simp, rclike_simps]
theorem mul_im : ∀ z w : K, im (z * w) = re z * im w + im z * re w :=
  RCLike.mul_im_ax

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

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

Разделы

Аффилиация

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