realPart_ofReal — Mathlib

English

The real part of the real number r, when viewed as a complex number, equals r itself.

Русский

Действительная часть вещественного числа r, если рассматривать r как комплексное число, равна самому r.

LaTeX

$$$\Re(r) \;\text{in } \mathbb{C} = r\quad (r \in \mathbb{R}).$$$

Lean4

@[simp]
theorem realPart_ofReal (r : ℝ) : (ℜ (r : ℂ) : ℂ) = r :=
  by
  rw [realPart_apply_coe, star_def, conj_ofReal, ← two_smul ℝ (r : ℂ)]
  simp

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