# `norm_num` extension for `Nat.sqrt` #

This module defines a `norm_num` extension for `Nat.sqrt`.

source
theorem Tactic.NormNum.nat_sqrt_helper {x y r : ℕ} (hr : y * y + r = x) (hle : r.ble (2 * y) = true) :
x.sqrt = y
source
theorem Tactic.NormNum.isNat_sqrt {x nx z : ℕ} :
Mathlib.Meta.NormNum.IsNat x nx → nx.sqrt = z → Mathlib.Meta.NormNum.IsNat x.sqrt z
source
def Tactic.NormNum.proveNatSqrt (ex : Q(ℕ)) :
(ey : Q(ℕ)) × Q(«$ex».sqrt = «$ey»)

Given the natural number literal `ex`, returns its square root as a natural number literal and an equality proof. Panics if `ex` isn't a natural number literal.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Tactic.NormNum.evalNatSqrt :
Mathlib.Meta.NormNum.NormNumExt

Evaluates the `Nat.sqrt` function.

Equations

- One or more equations did not get rendered due to their size.

Instances For