lean_workbook_plus_44792

Proved

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

Find the general term of the sequence $U_{2^{2h}} = [2^{2h}\sqrt{2^{2h}}] = 2^{3h}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_44792 (h : ℕ) : (2^(2 * h) * Real.sqrt ((2^(2 * h))) : ℝ) = 2^(3 * h)   :=  by sorry

Source