im_ofReal_mul

Mathlib.Data.Complex.Basic

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

English

The imaginary part of the product with a real scalar satisfies (r z).im = r z.im.

Русский

Мнимая часть произведения с действительным множителем удовлетворяет (r z).im = r z.im.

LaTeX

$$$(r z).im = r \cdot z.im$$

Lean4

theorem im_ofReal_mul (r : ℝ) (z : ℂ) : (r * z).im = r * z.im := by simp [ofReal]

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

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

Разделы

Аффилиация

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