Documentation

Mathlib.Tactic.NormNum.NatSqrt

norm_num extension for Nat.sqrt #

This module defines a norm_num extension for Nat.sqrt.

theorem Tactic.NormNum.nat_sqrt_helper {x : } {y : } {r : } (hr : y * y + r = x) (hle : r.ble (2 * y) = true) :
x.sqrt = y
theorem Tactic.NormNum.isNat_sqrt {x : } {nx : } {z : } :
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

    Evaluates the Nat.sqrt function.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For