im_nsmul — Mathlib

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 ..

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