Prove2Me

Lean-Workbook Plus 56339: Logarithmic inequality

Proved
WorkbookRestored.plus_56339

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

For real a,b≥1a,b\ge1, log⁡ab=1/log⁡ba\log_a b=1/\log_b a. The base logarithms are Lean’s total ratios of natural logarithms, including the exceptional base value one.

Source: Lean-Workbook row lean_workbook_plus_56339 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.

Preamble
import Mathlib.Analysis.SpecialFunctions.Log.Base
open Real
Formal statement
theorem WorkbookRestored.plus_56339 (a b : ℝ) (ha : 1 ≤ a) (hb : 1 ≤ b) : Real.logb a b = 1 / Real.logb b a   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_56339; immutable original Prove2Me node 951f0bbc-c1c0-4382-816f-69c91b2dab96

View graph