im_zsmul — Mathlib

English

For every integer n and complex z, the imaginary part of n-scalar multiplication equals n times the imaginary part.

Русский

Для каждого целого n и комплексного z мнимая часть удвоения на n равна n умножению мнимой части.

LaTeX

$$$\forall n \in \mathbb{Z}, z \in \mathbb{C}, \operatorname{Im}(n \cdot z) = n \cdot \operatorname{Im}(z)$$$

Lean4

theorem im_zsmul (n : ℤ) (z : ℂ) : (n • z).im = n • z.im :=
  smul_im ..

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