Loogle!

Result

Found 60 declarations mentioning Nat.sqrt.

• Nat.sqrt 📋 Batteries.Data.Nat.Basic
  (n : ℕ) : ℕ
• Nat.sqrt_le_self 📋 Mathlib.Data.Nat.Sqrt
  (n : ℕ) : n.sqrt ≤ n
• Nat.sqrt_succ_le_succ_sqrt 📋 Mathlib.Data.Nat.Sqrt
  (n : ℕ) : n.succ.sqrt ≤ n.sqrt.succ
• Nat.sqrt_one 📋 Mathlib.Data.Nat.Sqrt
  : Nat.sqrt 1 = 1
• Nat.sqrt_two 📋 Mathlib.Data.Nat.Sqrt
  : Nat.sqrt 2 = 1
• Nat.sqrt_zero 📋 Mathlib.Data.Nat.Sqrt
  : Nat.sqrt 0 = 0
• Nat.sqrt_eq 📋 Mathlib.Data.Nat.Sqrt
  (n : ℕ) : (n * n).sqrt = n
• Nat.sqrt_le_sqrt 📋 Mathlib.Data.Nat.Sqrt
  {m n : ℕ} (h : m ≤ n) : m.sqrt ≤ n.sqrt
• Nat.sqrt_le 📋 Mathlib.Data.Nat.Sqrt
  (n : ℕ) : n.sqrt * n.sqrt ≤ n
• Nat.sqrt_lt_self 📋 Mathlib.Data.Nat.Sqrt
  {n : ℕ} (h : 1 < n) : n.sqrt < n
• Nat.lt_succ_sqrt 📋 Mathlib.Data.Nat.Sqrt
  (n : ℕ) : n < n.sqrt.succ * n.sqrt.succ
• Nat.le_three_of_sqrt_eq_one 📋 Mathlib.Data.Nat.Sqrt
  {n : ℕ} (h : n.sqrt = 1) : n ≤ 3
• Nat.sqrt_eq_zero 📋 Mathlib.Data.Nat.Sqrt
  {n : ℕ} : n.sqrt = 0 ↔ n = 0
• Nat.sqrt_eq' 📋 Mathlib.Data.Nat.Sqrt
  (n : ℕ) : (n ^ 2).sqrt = n
• Nat.sqrt_pos 📋 Mathlib.Data.Nat.Sqrt
  {n : ℕ} : 0 < n.sqrt ↔ 0 < n
• Nat.le_sqrt 📋 Mathlib.Data.Nat.Sqrt
  {m n : ℕ} : m ≤ n.sqrt ↔ m * m ≤ n
• Nat.sqrt_le' 📋 Mathlib.Data.Nat.Sqrt
  (n : ℕ) : n.sqrt ^ 2 ≤ n
• Nat.sqrt_lt 📋 Mathlib.Data.Nat.Sqrt
  {m n : ℕ} : m.sqrt < n ↔ m < n * n
• Nat.lt_succ_sqrt' 📋 Mathlib.Data.Nat.Sqrt
  (n : ℕ) : n < n.sqrt.succ ^ 2
• Nat.add_one_sqrt_le_of_ne_zero 📋 Mathlib.Data.Nat.Sqrt
  {n : ℕ} (hn : n ≠ 0) : (n + 1).sqrt ≤ n
• Nat.le_sqrt_of_eq_mul 📋 Mathlib.Data.Nat.Sqrt
  {a b c : ℕ} (h : a = b * c) : b ≤ a.sqrt ∨ c ≤ a.sqrt
• Nat.sqrt_mul_sqrt_lt_succ 📋 Mathlib.Data.Nat.Sqrt
  (n : ℕ) : n.sqrt * n.sqrt < n + 1
• Nat.le_sqrt' 📋 Mathlib.Data.Nat.Sqrt
  {m n : ℕ} : m ≤ n.sqrt ↔ m ^ 2 ≤ n
• Nat.sqrt_lt' 📋 Mathlib.Data.Nat.Sqrt
  {m n : ℕ} : m.sqrt < n ↔ m < n ^ 2
• Nat.exists_mul_self 📋 Mathlib.Data.Nat.Sqrt
  (x : ℕ) : (∃ n, n * n = x) ↔ x.sqrt * x.sqrt = x
• Nat.sqrt_le_add 📋 Mathlib.Data.Nat.Sqrt
  (n : ℕ) : n ≤ n.sqrt * n.sqrt + n.sqrt + n.sqrt
• Nat.sqrt_mul_sqrt_lt_succ' 📋 Mathlib.Data.Nat.Sqrt
  (n : ℕ) : n.sqrt ^ 2 < n + 1
• Nat.sqrt_add_eq 📋 Mathlib.Data.Nat.Sqrt
  {a : ℕ} (n : ℕ) (h : a ≤ n + n) : (n * n + a).sqrt = n
• Nat.sqrt_add_eq' 📋 Mathlib.Data.Nat.Sqrt
  {a : ℕ} (n : ℕ) (h : a ≤ n + n) : (n ^ 2 + a).sqrt = n
• Nat.exists_mul_self' 📋 Mathlib.Data.Nat.Sqrt
  (x : ℕ) : (∃ n, n ^ 2 = x) ↔ x.sqrt ^ 2 = x
• Nat.succ_le_succ_sqrt' 📋 Mathlib.Data.Nat.Sqrt
  (n : ℕ) : n + 1 ≤ (n.sqrt + 1) ^ 2
• Nat.succ_le_succ_sqrt 📋 Mathlib.Data.Nat.Sqrt
  (n : ℕ) : n + 1 ≤ (n.sqrt + 1) * (n.sqrt + 1)
• Nat.eq_sqrt 📋 Mathlib.Data.Nat.Sqrt
  {n a : ℕ} : a = n.sqrt ↔ a * a ≤ n ∧ n < (a + 1) * (a + 1)
• Nat.eq_sqrt' 📋 Mathlib.Data.Nat.Sqrt
  {n a : ℕ} : a = n.sqrt ↔ a ^ 2 ≤ n ∧ n < (a + 1) ^ 2
• Nat.sqrt.eq_1 📋 Mathlib.Data.Nat.Sqrt
  (n : ℕ) : n.sqrt = if n ≤ 1 then n else Nat.sqrt.iter n (1 <<< (n.log2 / 2 + 1))
• Int.sqrt.eq_1 📋 Mathlib.Data.Int.Sqrt
  (z : ℤ) : Int.sqrt z = ↑z.toNat.sqrt
• Int.sqrt_natCast 📋 Mathlib.Data.Int.Sqrt
  (n : ℕ) : Int.sqrt ↑n = ↑n.sqrt
• Int.sqrt_ofNat 📋 Mathlib.Data.Int.Sqrt
  (n : ℕ) : Int.sqrt (OfNat.ofNat n) = ↑(OfNat.ofNat n).sqrt
• Nat.unpair.eq_1 📋 Mathlib.Data.Nat.Pairing
  (n : ℕ) : Nat.unpair n = if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)
• Nat.prime_def_le_sqrt 📋 Mathlib.Data.Nat.Prime.Defs
  {p : ℕ} : Nat.Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
• Nat.minFac_lemma 📋 Mathlib.Data.Nat.Prime.Defs
  (n k : ℕ) (h : ¬n < k * k) : n.sqrt - k < n.sqrt + 2 - k
• Real.nat_sqrt_le_real_sqrt 📋 Mathlib.Data.Real.Sqrt
  {a : ℕ} : ↑a.sqrt ≤ √↑a
• Real.floor_real_sqrt_eq_nat_sqrt 📋 Mathlib.Data.Real.Sqrt
  {a : ℕ} : ⌊√↑a⌋ = ↑a.sqrt
• Real.nat_floor_real_sqrt_eq_nat_sqrt 📋 Mathlib.Data.Real.Sqrt
  {a : ℕ} : ⌊√↑a⌋₊ = a.sqrt
• Real.real_sqrt_le_nat_sqrt_succ 📋 Mathlib.Data.Real.Sqrt
  {a : ℕ} : √↑a ≤ ↑a.sqrt + 1
• Real.real_sqrt_lt_nat_sqrt_succ 📋 Mathlib.Data.Real.Sqrt
  {a : ℕ} : √↑a < ↑a.sqrt + 1
• Nat.minSqFacAux.eq_1 📋 Mathlib.Data.Nat.Squarefree
  (x✝ x✝¹ : ℕ) : x✝.minSqFacAux x✝¹ = if h : x✝ < x✝¹ * x✝¹ then none else have this := ⋯; if x✝¹ ∣ x✝ then let n' := x✝ / x✝¹; have this := ⋯; if x✝¹ ∣ n' then some x✝¹ else n'.minSqFacAux (x✝¹ + 2) else x✝.minSqFacAux (x✝¹ + 2)
• Nat.minSqFacAux.eq_def 📋 Mathlib.Data.Nat.Squarefree
  (x✝ x✝¹ : ℕ) : x✝.minSqFacAux x✝¹ = match x✝, x✝¹ with | n, k => if h : n < k * k then none else have this := ⋯; if k ∣ n then let n' := n / k; have this := ⋯; if k ∣ n' then some k else n'.minSqFacAux (k + 2) else n.minSqFacAux (k + 2)
• Rat.sqrt.eq_1 📋 Mathlib.Data.Rat.Sqrt
  (q : ℚ) : Rat.sqrt q = mkRat (Int.sqrt q.num) q.den.sqrt
• Rat.sqrt_natCast 📋 Mathlib.Data.Rat.Sqrt
  (n : ℕ) : Rat.sqrt ↑n = ↑n.sqrt
• Rat.sqrt_ofNat 📋 Mathlib.Data.Rat.Sqrt
  (n : ℕ) : Rat.sqrt (OfNat.ofNat n) = ↑(Nat.sqrt (OfNat.ofNat n))
• Primrec.nat_sqrt 📋 Mathlib.Computability.Primrec
  : Primrec Nat.sqrt
• Nat.Primrec'.sqrt 📋 Mathlib.Computability.Primrec
  : Nat.Primrec' fun v => v.head.sqrt
• PosNum.minFacAux_to_nat 📋 Mathlib.Data.Num.Prime
  {fuel : ℕ} {n k : PosNum} (h : (↑n).sqrt < fuel + ↑k.bit1) : ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
• bertrand_main_inequality 📋 Mathlib.NumberTheory.Bertrand
  {n : ℕ} (n_large : 512 ≤ n) : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
• centralBinom_le_of_no_bertrand_prime 📋 Mathlib.NumberTheory.Bertrand
  (n : ℕ) (n_large : 2 < n) (no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p) : n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
• Nat.smoothNumbersUpTo_card_le 📋 Mathlib.NumberTheory.SmoothNumbers
  (N k : ℕ) : (N.smoothNumbersUpTo k).card ≤ 2 ^ k.primesBelow.card * N.sqrt
• Nat.smoothNumbersUpTo_subset_image 📋 Mathlib.NumberTheory.SmoothNumbers
  (N k : ℕ) : N.smoothNumbersUpTo k ⊆ Finset.image (fun x => match x with | (s, m) => m ^ 2 * s.prod id) (k.primesBelow.powerset ×ˢ (Finset.range (N.sqrt + 1)).erase 0)
• Tactic.NormNum.isNat_sqrt 📋 Mathlib.Tactic.NormNum.NatSqrt
  {x nx z : ℕ} : Mathlib.Meta.NormNum.IsNat x nx → nx.sqrt = z → Mathlib.Meta.NormNum.IsNat x.sqrt z
• Tactic.NormNum.nat_sqrt_helper 📋 Mathlib.Tactic.NormNum.NatSqrt
  {x y r : ℕ} (hr : y * y + r = x) (hle : r.ble (2 * y) = true) : x.sqrt = y

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 6ff4759 serving mathlib revision 1c119a3