norm_num extension for Real.sqrt

This module defines a norm_num extension for Real.sqrt and NNReal.sqrt.

theorem Mathlib.Meta.NormNum.isNat_realSqrt {x : ℝ} {nx ny : ℕ} (h : IsNat x nx) (hy : ny * ny = nx) : IsNat (√x) ny

theorem Mathlib.Meta.NormNum.isNat_nnrealSqrt {x : NNReal} {nx ny : ℕ} (h : IsNat x nx) (hy : ny * ny = nx) : IsNat (NNReal.sqrt x) ny

theorem Mathlib.Meta.NormNum.isNNRat_nnrealSqrt_of_isNNRat {x : NNReal} {n sn d sd : ℕ} (hn : sn * sn = n) (hd : sd * sd = d) (h : IsNNRat x n d) : IsNNRat (NNReal.sqrt x) sn sd

theorem Mathlib.Meta.NormNum.isNat_realSqrt_neg {x : ℝ} {nx : ℕ} (h : IsInt x (Int.negOfNat nx)) : IsNat (√x) 0

theorem Mathlib.Meta.NormNum.isNat_realSqrt_of_isRat_negOfNat {x : ℝ} {num denom : ℕ} (h : IsRat x (Int.negOfNat num) denom) : IsNat (√x) 0

theorem Mathlib.Meta.NormNum.isNNRat_realSqrt_of_isNNRat {x : ℝ} {n sn d sd : ℕ} (hn : sn * sn = n) (hd : sd * sd = d) (h : IsNNRat x n d) : IsNNRat (√x) sn sd

def Mathlib.Meta.NormNum.evalRealSqrt : NormNumExt

norm_num extension that evaluates the function Real.sqrt.

Equations

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

def Mathlib.Meta.NormNum.evalNNRealSqrt : NormNumExt

norm_num extension that evaluates the function NNReal.sqrt.

Equations

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