Prove2Me

lean_workbook_plus_21774

Open

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

Prove the logarithmic identity: (log⁡ab)(log⁡bc)=log⁡ac(\log_a b)(\log_b c)=\log_a c

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_21774 : ∀ a b c : ℝ, (a > 0 ∧ b > 0 ∧ c > 0 ∧ a ≠ 1 ∧ b ≠ 1 ∧ c ≠ 1) →  (Real.log b / Real.log a) * (Real.log c / Real.log b) = (Real.log c / Real.log a)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph