coe_realPart — Mathlib

English

The real-part projection is compatible with complex multiplication by a real scalar, and it picks out the real part of a complex number.

Русский

Проекция вещественной части совместима с умножением комплексного числа на вещественный коэффициент и извлекает вещественную часть комплексного числа.

LaTeX

$$$\Re(z) = \operatorname{Re}(z) \quad (z \in \mathbb{C}).$$$

Lean4

theorem coe_realPart (z : ℂ) : (ℜ z : ℂ) = z.re :=
  calc
    (ℜ z : ℂ) = (↑(ℜ (↑z.re + ↑z.im * I))) := by congrm (ℜ $((re_add_im z).symm))
    _ = z.re := by
      rw [map_add, AddSubmonoid.coe_add, mul_comm, ← smul_eq_mul, realPart_I_smul]
      simp

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