log_mul — Mathlib

English

Let x, y be real numbers with x ≠ 0 and y ≠ 0. Then log(xy) = log x + log y.

Русский

Пусть x, y — вещественные числа и x ≠ 0, y ≠ 0. Тогда log(xy) = log x + log y.

LaTeX

$$$$ \log(xy) = \log x + \log y \\quad \text{for } x \neq 0,\ y \neq 0.$$$$

Lean4

theorem log_mul (hx : x ≠ 0) (hy : y ≠ 0) : log (x * y) = log x + log y :=
  exp_injective <| by rw [exp_log_eq_abs (mul_ne_zero hx hy), exp_add, exp_log_eq_abs hx, exp_log_eq_abs hy, abs_mul]

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