norm_num extension for IsSquare

The extension in this file handles natural, integer, and rational numbers.

TODO

Add extensions for ℚ≥0, ℝ, ℝ≥0, ℝ≥0∞, ℂ (or any algebraically closed field?), ZMod n. Probably, these extensions should go to different files.

theorem Mathlib.Meta.NormNum.isSquare_nat_of_isNat (a n : ℕ) (h : IsNat a n) (m : ℕ) (hm : m * m = n) : IsSquare a

theorem Mathlib.Meta.NormNum.not_isSquare_nat_of_isNat (a n : ℕ) (h : IsNat a n) (m k : ℕ) (hm : m * m = k) (hk₁ : k.blt n = true) (hk₂ : n.ble (k + 2 * m) = true) : ¬IsSquare a

If m ^ 2 < n < (m + 1) ^ 2, then n is not a square. We write this condition as k < n ≤ k + 2 * m, where k = m * m.

theorem Mathlib.Meta.NormNum.iff_isSquare_int_of_isNat (a : ℤ) (n : ℕ) (h : IsNat a n) : IsSquare n ↔ IsSquare a

theorem Mathlib.Meta.NormNum.iff_isSquare_of_isInt_int (a : ℤ) (n : ℕ) (h : IsInt a (Int.negOfNat n)) : n = 0 ↔ IsSquare a

theorem Mathlib.Meta.NormNum.iff_isSquare_of_isNat_rat (a : ℚ) (n : ℕ) (h : IsNat a n) : IsSquare n ↔ IsSquare a

theorem Mathlib.Meta.NormNum.iff_isSquare_of_isInt_rat (a : ℚ) (n : ℕ) (h : IsInt a (Int.negOfNat n)) : n = 0 ↔ IsSquare a

theorem Mathlib.Meta.NormNum.isSquare_of_isNNRat_rat (a : ℚ) (n d : ℕ) (hn : IsSquare n) (hd : IsSquare d) (ha : IsNNRat a n d) : IsSquare a

theorem Mathlib.Meta.NormNum.not_isSquare_of_isNNRat_rat_of_num (a : ℚ) (n d : ℕ) (hn : ¬IsSquare n) (hnd : n.Coprime d) (ha : IsNNRat a n d) : ¬IsSquare a

theorem Mathlib.Meta.NormNum.not_isSquare_of_isNNRat_rat_of_den (a : ℚ) (n d : ℕ) (hd : ¬IsSquare d) (hnd : n.Coprime d) (ha : IsNNRat a n d) : ¬IsSquare a

theorem Mathlib.Meta.NormNum.not_isSquare_of_isRat_neg (a : ℚ) (n d : ℕ) (hn : n ≠ 0) (hd : d ≠ 0) (ha : IsRat a (Int.negOfNat n) d) : ¬IsSquare a

def Mathlib.Meta.NormNum.evalIsSquareNat : NormNumExt

norm_num extension for IsSquare on ℕ.

def Mathlib.Meta.NormNum.evalIsSquareInt : NormNumExt

norm_num extension for IsSquare on ℤ.

def Mathlib.Meta.NormNum.evalIsSquareRat : NormNumExt

norm_num extension for IsSquare on ℚ.