ofReal_log — Mathlib

English

The real part of the complex logarithm of a real number equals the real logarithm of that number.

Русский

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

LaTeX

$$$$\\Re(\\log(x)) = \\operatorname{Real.log}(x) \\quad \\text{for } x \\in \\mathbb{R}.$$$$

Lean4

theorem ofReal_log {x : ℝ} (hx : 0 ≤ x) : (x.log : ℂ) = log x :=
  Complex.ext (by rw [log_re, ofReal_re, Complex.norm_of_nonneg hx])
    (by rw [ofReal_im, log_im, arg_ofReal_of_nonneg hx])

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