log_mul_ofReal — Mathlib

English

If x, y ∈ ℂ lie in the strip -π < Im(·) ≤ π and exp x = exp y, then x = y.

Русский

Если x, y ∈ ℂ лежат в полосе -π < Im(·) ≤ π и exp x = exp y, то x = y.

LaTeX

$$$\text{If } -\pi < \operatorname{Im}(x) \le \pi \text{ and } -\pi < \operatorname{Im}(y) \le \pi,\ \exp x = \exp y \Rightarrow x = y.$$$

Lean4

theorem log_mul_ofReal (r : ℝ) (hr : 0 < r) (x : ℂ) (hx : x ≠ 0) : log (x * r) = Real.log r + log x := by
  rw [mul_comm, log_ofReal_mul hr hx]

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