logb_mul_base — Mathlib

English

Log with base of a product equals the inverse-sum expression: log_b(ab) c = ((log_b a c)^{-1} + (log_b b c)^{-1})^{-1}.

Русский

Логарифм по основанию b от произведения ab равен обратному выражению суммы: log_b(ab) c = ((log_b a c)^{-1} + (log_b b c)^{-1})^{-1}.

LaTeX

$$$\log_b(ab) c = \big((\log_b a c)^{-1} + (\log_b b c)^{-1}\big)^{-1}$$$

Lean4

theorem logb_mul_base {a b : ℝ} (h₁ : a ≠ 0) (h₂ : b ≠ 0) (c : ℝ) : logb (a * b) c = ((logb a c)⁻¹ + (logb b c)⁻¹)⁻¹ :=
  by rw [← inv_logb_mul_base h₁ h₂ c, inv_inv]

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