lean_workbook_plus_44231

Proved

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

We find that $5^n=3125\implies n=\boxed{5}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_44231  (n : ℕ)
  (h₀ : 5^n = 3125) :
  n = 5   :=  by sorry

Source