im_ofReal_mul

Mathlib.Analysis.RCLike.Basic

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

English

For r ∈ ℝ and z ∈ K, Im (↑r * z) = r * Im z.

Русский

Для r ∈ ℝ и z ∈ K, мнимая часть произведения равна произведению r и мнимой части z.

LaTeX

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

Lean4

@[rclike_simps]
theorem im_ofReal_mul (r : ℝ) (z : K) : im (↑r * z) = r * im z := by
  simp only [add_zero, ofReal_im, zero_mul, ofReal_re, mul_im]

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

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

Разделы

Аффилиация

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