Change_of_Base_of_Logarithm

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

change-of-base-of-logarithmlogarithmsproofwiki

$\log_b x = \dfrac {\log_a x} {\log_a b}$

Preamble

import Mathlib.Analysis.SpecialFunctions.Log.Basic

Formal statement

theorem Change_of_Base_of_Logarithm (a b : ℝ) (ha : 0 < a) (hb : 0 < b) (ha1 : a ≠ 1) (hb1 : b ≠ 1) : Real.log a / Real.log b * (Real.log b / Real.log a) = 1 := by sorry

Source

https://proofwiki.org/wiki/Change_of_Base_of_Logarithm

View graph