mul_re

Mathlib.Analysis.RCLike.Basic

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

English

The real part of a product satisfies re(z w) = re z re w − im z im w.

Русский

Действительная часть произведения удовлетворяет re(z w) = re(z) re(w) − im(z) im(w).

LaTeX

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

Lean4

@[simp, rclike_simps]
theorem mul_re : ∀ z w : K, re (z * w) = re z * re w - im z * im w :=
  RCLike.mul_re_ax

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

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

Разделы

Аффилиация

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