Recovering a logarithm from a linear relation

Proved

WorkbookRestored.plus_738

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

lean-workbookrestored-importssource-checked

Let $r$ be real. If $\log5=r\log2$ , then

r=\log_2 5.

Formalization Note This restores source entry lean_workbook_plus_738 from the Apache-2.0 Lean-Workbook dataset. The mathematical proposition is unchanged; targeted imports and namespace openings supply the constants missing from the original Prove2Me node 25110978-ff41-4f3e-9a23-51425715a12b. This is a separate corrected node because formal statements and preambles are immutable.

Preamble

import Mathlib.Analysis.SpecialFunctions.Log.Base
import Mathlib.Tactic
open Real

Formal statement

theorem WorkbookRestored.plus_738  (r : ℝ)
  (h₀ : Real.log 5 = r * Real.log 2) :
  r = Real.logb 2 5   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_738; original Prove2Me theorem ID 25110978-ff41-4f3e-9a23-51425715a12b; Apache-2.0.

View graph