mul_logb — Mathlib

English

The ratio of two logarithms with the same base equals the logarithm with the base of the ratio: log_b a c / log_b b c = log_b a b, provided the denominator is nonzero.

Русский

Отношение двух логарифмов одного основания равно логарифму по основанию отношения: log_b a c / log_b b c = log_b a b, если знаменатель не нулевой.

LaTeX

$$$\dfrac{\log_b a c}{\log_b b c} = \log_b a b$$$

Lean4

theorem mul_logb {a b c : ℝ} (h₁ : b ≠ 0) (h₂ : b ≠ 1) (h₃ : b ≠ -1) : logb a b * logb b c = logb a c :=
  by
  unfold logb
  rw [mul_comm, div_mul_div_cancel₀ (log_ne_zero.mpr ⟨h₁, h₂, h₃⟩)]

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