inv_logb_mul_base — Mathlib

English

Inverse of log base of a product equals sum of inverses of logs: (log_b(ab) c)^{-1} = (log_b a c)^{-1} + (log_b b c)^{-1}.

Русский

(log_b(ab) c)^{-1} = (log_b a c)^{-1} + (log_b b c)^{-1}.

LaTeX

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

Lean4

theorem inv_logb_mul_base {a b : ℝ} (h₁ : a ≠ 0) (h₂ : b ≠ 0) (c : ℝ) :
    (logb (a * b) c)⁻¹ = (logb a c)⁻¹ + (logb b c)⁻¹ := by simp_rw [inv_logb]; exact logb_mul h₁ h₂

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