log_div — Mathlib

English

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

Русский

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

LaTeX

$$$$ \log\left(\frac{x}{y}\right) = \log x - \log y \quad \text{for } x \neq 0,\ y \neq 0.$$$$

Lean4

theorem log_div (hx : x ≠ 0) (hy : y ≠ 0) : log (x / y) = log x - log y :=
  exp_injective <| by rw [exp_log_eq_abs (div_ne_zero hx hy), exp_sub, exp_log_eq_abs hx, exp_log_eq_abs hy, abs_div]

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