re_ofReal_mul

Mathlib.Data.Complex.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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