lean_workbook_plus_63077

Proved

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

I am sorry, it should be stated that $p$ is prime and $m$ integer. Thank you riddler

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_63077 (p : ℕ) (hp : p.Prime) (m : ℤ) : (∃ n : ℕ, (n : ℤ)^2 = m * p) ↔ ∃ t : ℤ, t^2 = m * p   :=  by sorry

Source