instMul

Mathlib.Data.Complex.Basic

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

English

The product of complex numbers z = a + bi and w = c + di is z w = (ac - bd) + (ad + bc)i.

Русский

Произведение комплексных чисел z = a + bi и w = c + di равняется z w = (ac - bd) + (ad + bc)i.

LaTeX

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

Lean4

instance : Mul ℂ :=
  ⟨fun z w => ⟨z.re * w.re - z.im * w.im, z.re * w.im + z.im * w.re⟩⟩

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

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

Разделы

Аффилиация

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