lean_workbook_plus_66898
OpenWe can rewrite as . This works as if we write , then . Taking the square root, .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_66898 : Real.logb 4 6 = Real.logb 2 (Real.sqrt 6) := by sorry
Source