mathlib3 documentation


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.

theorem norm_num.is_sqrt {n a a2 b : } (ha2 : a * a = a2) (hb : a2 + b = n) (hle : b bit0 a) :

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

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