smul_im

Mathlib.Data.Complex.Basic

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

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_im (r : R) (z : ℂ) : (r • z).im = r • z.im := by simp [(· • ·), SMul.smul]

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

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

Разделы

Аффилиация

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