mathlib3 documentation

data.nat.sqrt_norm_num

norm_num plugin for sqrt #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The norm_num plugin evaluates sqrt by bounding it between consecutive integers.

source
theorem norm_num.is_sqrt {n a a2 b : ℕ} (ha2 : a * a = a2) (hb : a2 + b = n) (hle : b ≤ bit0 a) :
nat.sqrt n = a
source
meta def norm_num.prove_sqrt (ic : tactic.instance_cache) (n : expr) :
tactic (tactic.instance_cache × expr × expr)

Given n provides (a, ⊢ nat.sqrt n = a).

source
meta def norm_num.eval_sqrt  :
expr → tactic (expr × expr)

A norm_num plugin for sqrt n when n is a numeral.