norm_num extension for Real.sqrt #
This module defines a norm_num extension for Real.sqrt and NNReal.sqrt.
Implementation notes #
While the extension for Real.sqrt can handle both integers and rationals, the one for
NNReal.sqrt can only deal with integers, due to a limitation of norm_num
(i.e. the IsRat type requires a Ring instance).
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)
:
theorem
Tactic.NormNum.isNat_realSqrt_neg
{x : ℝ}
{nx : ℕ}
(h : Mathlib.Meta.NormNum.IsInt x (Int.negOfNat nx))
:
theorem
Tactic.NormNum.isNat_realSqrt_of_isRat_negOfNat
{x : ℝ}
{num denom : ℕ}
(h : Mathlib.Meta.NormNum.IsRat x (Int.negOfNat num) denom)
:
theorem
Tactic.NormNum.isRat_realSqrt_of_isRat_ofNat
{x : ℝ}
{n sn d sd : ℕ}
(hn : sn * sn = n)
(hd : sd * sd = d)
(h : Mathlib.Meta.NormNum.IsRat x (Int.ofNat n) d)
:
Mathlib.Meta.NormNum.IsRat (√x) (Int.ofNat sn) sd
norm_num extension that evaluates the function NNReal.sqrt.