English
For every natural 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{N}, z \in \mathbb{C}, \operatorname{Im}(n \cdot z) = n \cdot \operatorname{Im}(z)$$$
Lean4
theorem im_nsmul (n : ℕ) (z : ℂ) : (n • z).im = n • z.im :=
smul_im ..