re_nsmul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem re_nsmul (n : ℕ) (z : ℂ) : (n • z).re = n • z.re :=
  smul_re ..

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