Lean-Workbook Plus 26180: Logarithmic inequality

Proved

WorkbookRestored.plus_26180

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

lean-workbookrestored-importssource-checked

For $x,a,b>0$ , $\log_x a-\log_x b=\log_x(a/b)$ . Here $\log_x t$ denotes Lean’s total ratio $\log t/\log x$ , so the statement also includes $x=1$ .

Source: Lean-Workbook row lean_workbook_plus_26180 (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_26180 (x a b : ℝ) (hx : x > 0) (hab : a > 0 ∧ b > 0) : Real.logb x a - Real.logb x b = Real.logb x (a / b)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_26180; immutable original Prove2Me node 0121a0cc-64a0-40e9-8816-ed0b40fdc56e

View graph