lean_workbook_plus_8149

Proved

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

b) $\frac{n^n}{(2^n)^2}= \frac{n^n}{2^{2n}}= ( \frac{n}{4} )^n$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_8149 (n : ℕ) : (n^n / (2^n)^2 : ℝ) = (n / 4)^n   :=  by sorry

Source