log_mul — Mathlib

English

For powers x and y with base n, the log of their product equals the sum of the logs: log(x*y) = log x + log y.

Русский

Для степеней x и y с основанием n логарифм произведения равен сумме логарифмов: log(xy) = log x + log y.

LaTeX

$$$ \\log(x\\cdot y) = \\log x + \\log y $$$

Lean4

theorem log_mul [DecidableEq M] {n : M} (h : Function.Injective fun m : ℕ => n ^ m) (x y : powers (n : M)) :
    log (x * y) = log x + log y :=
  map_mul (powLogEquiv h).symm x y

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