lean_workbook_plus_73621

Proved

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

$\\sqrt{k}$ is an integer if and only if $k$ is a perfect square (k is the square of an integer).

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_73621 (k : ℕ) : (∃ x : ℕ, x^2 = k) ↔ (∃ x : ℕ, x = Real.sqrt k)   :=  by sorry

Source