Prove2Me

lean_workbook_plus_20863

Open

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

Prove (log⁡ab)×(log⁡cd)=(log⁡cb)×(log⁡ad) (\log_{a}b) \times (\log_{c}d) = (\log_{c}b) \times (\log_{a}d)

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_20863 (a b c d : ℝ) : (Real.log b / Real.log a) * (Real.log d / Real.log c) = (Real.log b / Real.log c) * (Real.log d / Real.log a)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph