smul_re

Mathlib.Data.Complex.Basic

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

English

Im(r • z) = r • Im(z) for a scalar r ∈ R.

Русский

Im( r • z ) = r • Im(z) для скаляра r ∈ R.

LaTeX

$$$\\operatorname{Im}(r \\cdot z) = r \\cdot \\operatorname{Im}(z)$$$

Lean4

theorem smul_re (r : R) (z : ℂ) : (r • z).re = r • z.re := by simp [(· • ·), SMul.smul]

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

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

Разделы

Аффилиация

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