Documentation

Mathlib.Tactic.NormNum.IsSquare

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.

source
theorem Mathlib.Meta.NormNum.isSquare_nat_of_isNat (a n : ℕ) (h : IsNat a n) (m : ℕ) (hm : m * m = n) :
IsSquare a
source
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.

source
theorem Mathlib.Meta.NormNum.iff_isSquare_int_of_isNat (a : ℤ) (n : ℕ) (h : IsNat a n) :
IsSquare n ↔ IsSquare a
source
theorem Mathlib.Meta.NormNum.iff_isSquare_of_isInt_int (a : ℤ) (n : ℕ) (h : IsInt a (Int.negOfNat n)) :
n = 0 ↔ IsSquare a
source
theorem Mathlib.Meta.NormNum.iff_isSquare_of_isNat_rat (a : ℚ) (n : ℕ) (h : IsNat a n) :
IsSquare n ↔ IsSquare a
source
theorem Mathlib.Meta.NormNum.iff_isSquare_of_isInt_rat (a : ℚ) (n : ℕ) (h : IsInt a (Int.negOfNat n)) :
n = 0 ↔ IsSquare a
source
theorem Mathlib.Meta.NormNum.isSquare_of_isNNRat_rat (a : ℚ) (n d : ℕ) (hn : IsSquare n) (hd : IsSquare d) (ha : IsNNRat a n d) :
IsSquare a
source
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
source
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
source
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
source
def Mathlib.Meta.NormNum.evalIsSquareNat :
NormNumExt

norm_num extension for IsSquare on ℕ.

Instances For
    source
    def Mathlib.Meta.NormNum.evalIsSquareInt :
    NormNumExt

    norm_num extension for IsSquare on ℤ.

    Instances For
      source
      def Mathlib.Meta.NormNum.evalIsSquareRat :
      NormNumExt

      norm_num extension for IsSquare on ℚ.

      Instances For