lean_workbook_plus_25042

Open

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

So what remains is: $\log_2(\log_4 (16) ) = \log_2(2) = \boxed{1}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_25042 :
  Real.logb 2 (Real.logb 4 16) = 1   :=  by sorry

Source