re_ofReal_mul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[rclike_simps]
theorem re_ofReal_mul (r : ℝ) (z : K) : re (↑r * z) = r * re z := by
  simp only [mul_re, ofReal_im, zero_mul, ofReal_re, sub_zero]

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