lean_workbook_plus_72336

Proved

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

If $x$ is a perfect square, then $x^n$ will be a perfect square no matter what n is.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_72336 (x : ℕ) (n : ℕ) (hx : ∃ t, t^2 = x) : ∃ t, t^2 = x^n   :=  by sorry

Source