Documentation

Mathlib.Tactic.NormNum.NatSqrt

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 : Nat.ble r (2 * y) = true) :
Nat.sqrt x = y
source
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
source
def Tactic.NormNum.proveNatSqrt (ex : Q(ℕ)) :
(ey : Q(ℕ)) × Q(Nat.sqrt «$ex» = «$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