norm_num extension for Real.sqrt

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

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

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

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

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

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

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

def Tactic.NormNum.evalRealSqrt : Mathlib.Meta.NormNum.NormNumExt

norm_num extension that evaluates the function Real.sqrt.

Equations

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

def Tactic.NormNum.evalNNRealSqrt : Mathlib.Meta.NormNum.NormNumExt

norm_num extension that evaluates the function NNReal.sqrt.

Equations

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