theorem
Tactic.NormNum.isNat_sqrt
{x : ℕ}
{nx : ℕ}
{z : ℕ}
:
Mathlib.Meta.NormNum.IsNat x nx → Nat.sqrt nx = z → Mathlib.Meta.NormNum.IsNat (Nat.sqrt x) z
Evaluates the Nat.sqrt
function.
Mathlib.Tactic.NormNum.NatSqrt
Evaluates the Nat.sqrt
function.