lean_workbook_plus_56177

Proved

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

Show that $\left(\frac{2010}{2009}\right)^{2009}> 2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_56177 : (2010 / 2009 : ℝ) ^ (2009:ℕ) > 2   :=  by sorry

Source