Loogle!

Result

Found 2219 declarations mentioning Nat.Prime. Of these, only the first 200 are shown.

• Nat.Prime 📋 Mathlib.Data.Nat.Prime.Defs
  (p : ℕ) : Prop
• Nat.decidablePrime 📋 Mathlib.Data.Nat.Prime.Defs
  (p : ℕ) : Decidable (Nat.Prime p)
• Nat.decidablePrime' 📋 Mathlib.Data.Nat.Prime.Defs
  (p : ℕ) : Decidable (Nat.Prime p)
• Nat.prime_eleven 📋 Mathlib.Data.Nat.Prime.Defs
  : Nat.Prime 11
• Nat.prime_five 📋 Mathlib.Data.Nat.Prime.Defs
  : Nat.Prime 5
• Nat.prime_seven 📋 Mathlib.Data.Nat.Prime.Defs
  : Nat.Prime 7
• Nat.prime_three 📋 Mathlib.Data.Nat.Prime.Defs
  : Nat.Prime 3
• Nat.prime_two 📋 Mathlib.Data.Nat.Prime.Defs
  : Nat.Prime 2
• Nat.decidablePrime_csimp 📋 Mathlib.Data.Nat.Prime.Defs
  : Nat.decidablePrime = Nat.decidablePrime'
• Nat.fact_prime_three 📋 Mathlib.Data.Nat.Prime.Defs
  : Fact (Nat.Prime 3)
• Nat.fact_prime_two 📋 Mathlib.Data.Nat.Prime.Defs
  : Fact (Nat.Prime 2)
• Nat.not_prime_one 📋 Mathlib.Data.Nat.Prime.Defs
  : ¬Nat.Prime 1
• Nat.not_prime_zero 📋 Mathlib.Data.Nat.Prime.Defs
  : ¬Nat.Prime 0
• Nat.prime_one_false 📋 Mathlib.Data.Nat.Prime.Defs
  : Nat.Prime 1 → False
• Nat.prime_zero_false 📋 Mathlib.Data.Nat.Prime.Defs
  : Nat.Prime 0 → False
• Prime.nat_prime 📋 Mathlib.Data.Nat.Prime.Defs
  {p : ℕ} : Prime p → Nat.Prime p
• Nat.Prime.prime 📋 Mathlib.Data.Nat.Prime.Defs
  {p : ℕ} : Nat.Prime p → Prime p
• Nat.irreducible_iff_nat_prime 📋 Mathlib.Data.Nat.Prime.Defs
  (a : ℕ) : Irreducible a ↔ Nat.Prime a
• Nat.prime_iff 📋 Mathlib.Data.Nat.Prime.Defs
  {p : ℕ} : Nat.Prime p ↔ Prime p
• Nat.Prime.minFac_eq 📋 Mathlib.Data.Nat.Prime.Defs
  {p : ℕ} (hp : Nat.Prime p) : p.minFac = p
• Nat.Prime.ne_one 📋 Mathlib.Data.Nat.Prime.Defs
  {p : ℕ} (hp : Nat.Prime p) : p ≠ 1
• Nat.Prime.ne_zero 📋 Mathlib.Data.Nat.Prime.Defs
  {n : ℕ} (h : Nat.Prime n) : n ≠ 0
• Nat.minFac_prime 📋 Mathlib.Data.Nat.Prime.Defs
  {n : ℕ} (n1 : n ≠ 1) : Nat.Prime n.minFac
• Nat.Prime.one_le 📋 Mathlib.Data.Nat.Prime.Defs
  {p : ℕ} (hp : Nat.Prime p) : 1 ≤ p
• Nat.Prime.one_lt 📋 Mathlib.Data.Nat.Prime.Defs
  {p : ℕ} : Nat.Prime p → 1 < p
• Nat.Prime.pos 📋 Mathlib.Data.Nat.Prime.Defs
  {p : ℕ} (pp : Nat.Prime p) : 0 < p
• Nat.Prime.two_le 📋 Mathlib.Data.Nat.Prime.Defs
  {p : ℕ} : Nat.Prime p → 2 ≤ p
• Nat.Primes.coe_nat_injective 📋 Mathlib.Data.Nat.Prime.Defs
  : Function.Injective Subtype.val
• Nat.minFac_prime_iff 📋 Mathlib.Data.Nat.Prime.Defs
  {n : ℕ} : Nat.Prime n.minFac ↔ n ≠ 1
• Nat.Prime.not_dvd_one 📋 Mathlib.Data.Nat.Prime.Defs
  {p : ℕ} (pp : Nat.Prime p) : ¬p ∣ 1
• Nat.Prime.coprime_iff_not_dvd 📋 Mathlib.Data.Nat.Prime.Defs
  {p n : ℕ} (pp : Nat.Prime p) : p.Coprime n ↔ ¬p ∣ n
• Nat.Prime.one_lt' 📋 Mathlib.Data.Nat.Prime.Defs
  (p : ℕ) [hp : Fact (Nat.Prime p)] : Fact (1 < p)
• Nat.prime_dvd_prime_iff_eq 📋 Mathlib.Data.Nat.Prime.Defs
  {p q : ℕ} (pp : Nat.Prime p) (qp : Nat.Prime q) : p ∣ q ↔ p = q
• Nat.coprime_of_dvd 📋 Mathlib.Data.Nat.Prime.Defs
  {m n : ℕ} (H : ∀ (k : ℕ), Nat.Prime k → k ∣ m → ¬k ∣ n) : m.Coprime n
• Nat.prime_def_minFac 📋 Mathlib.Data.Nat.Prime.Defs
  {p : ℕ} : Nat.Prime p ↔ 2 ≤ p ∧ p.minFac = p
• Nat.exists_prime_and_dvd 📋 Mathlib.Data.Nat.Prime.Defs
  {n : ℕ} (hn : n ≠ 1) : ∃ p, Nat.Prime p ∧ p ∣ n
• Nat.not_prime_iff_minFac_lt 📋 Mathlib.Data.Nat.Prime.Defs
  {n : ℕ} (n2 : 2 ≤ n) : ¬Nat.Prime n ↔ n.minFac < n
• Nat.Primes.coe_nat_inj 📋 Mathlib.Data.Nat.Prime.Defs
  (p q : Nat.Primes) : ↑p = ↑q ↔ p = q
• Nat.Prime.eq_one_or_self_of_dvd 📋 Mathlib.Data.Nat.Prime.Defs
  {p : ℕ} (pp : Nat.Prime p) (m : ℕ) (hm : m ∣ p) : m = 1 ∨ m = p
• Nat.dvd_prime 📋 Mathlib.Data.Nat.Prime.Defs
  {p m : ℕ} (pp : Nat.Prime p) : m ∣ p ↔ m = 1 ∨ m = p
• Nat.dvd_prime_two_le 📋 Mathlib.Data.Nat.Prime.Defs
  {p m : ℕ} (pp : Nat.Prime p) (H : 2 ≤ m) : m ∣ p ↔ m = p
• Nat.minFac_le_div 📋 Mathlib.Data.Nat.Prime.Defs
  {n : ℕ} (pos : 0 < n) (np : ¬Nat.Prime n) : n.minFac ≤ n / n.minFac
• Nat.prime_of_coprime 📋 Mathlib.Data.Nat.Prime.Defs
  (n : ℕ) (h1 : 1 < n) (h : ∀ m < n, m ≠ 0 → n.Coprime m) : Nat.Prime n
• Nat.Prime.dvd_or_dvd 📋 Mathlib.Data.Nat.Prime.Defs
  {p m n : ℕ} (pp : Nat.Prime p) : p ∣ m * n → p ∣ m ∨ p ∣ n
• Nat.Prime.dvd_mul 📋 Mathlib.Data.Nat.Prime.Defs
  {p m n : ℕ} (pp : Nat.Prime p) : p ∣ m * n ↔ p ∣ m ∨ p ∣ n
• Nat.le_minFac 📋 Mathlib.Data.Nat.Prime.Defs
  {m n : ℕ} : n = 1 ∨ m ≤ n.minFac ↔ ∀ (p : ℕ), Nat.Prime p → p ∣ n → m ≤ p
• Nat.prime_def 📋 Mathlib.Data.Nat.Prime.Defs
  {p : ℕ} : Nat.Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
• Nat.prime_def_lt 📋 Mathlib.Data.Nat.Prime.Defs
  {p : ℕ} : Nat.Prime p ↔ 2 ≤ p ∧ ∀ m < p, m ∣ p → m = 1
• Nat.prime_def_lt' 📋 Mathlib.Data.Nat.Prime.Defs
  {p : ℕ} : Nat.Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), 2 ≤ m → m < p → ¬m ∣ p
• Nat.minFac_sq_le_self 📋 Mathlib.Data.Nat.Prime.Defs
  {n : ℕ} (w : 0 < n) (h : ¬Nat.Prime n) : n.minFac ^ 2 ≤ n
• 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.prime_iff_not_exists_mul_eq 📋 Mathlib.Data.Nat.Prime.Defs
  {p : ℕ} : Nat.Prime p ↔ 2 ≤ p ∧ ¬∃ m n, m < p ∧ n < p ∧ m * n = p
• ExpChar.prime 📋 Mathlib.Algebra.CharP.Defs
  {R : Type u_1} [AddMonoidWithOne R] {q : ℕ} (hprime : Nat.Prime q) [hchar : CharP R q] : ExpChar R q
• expChar_prime 📋 Mathlib.Algebra.CharP.Defs
  (R : Type u_1) [AddMonoidWithOne R] (p : ℕ) [CharP R p] [Fact (Nat.Prime p)] : ExpChar R p
• expChar_is_prime_or_one 📋 Mathlib.Algebra.CharP.Defs
  (R : Type u_1) [AddMonoidWithOne R] (q : ℕ) [hq : ExpChar R q] : Nat.Prime q ∨ q = 1
• char_eq_expChar_iff 📋 Mathlib.Algebra.CharP.Defs
  (R : Type u_1) [AddMonoidWithOne R] (p q : ℕ) [hp : CharP R p] [hq : ExpChar R q] : p = q ↔ Nat.Prime p
• CharP.char_is_prime_of_pos 📋 Mathlib.Algebra.CharP.Defs
  (R : Type u_1) [NonAssocSemiring R] [NoZeroDivisors R] [Nontrivial R] (p : ℕ) [NeZero p] [CharP R p] : Fact (Nat.Prime p)
• CharP.char_is_prime_of_two_le 📋 Mathlib.Algebra.CharP.Defs
  (R : Type u_1) [NonAssocSemiring R] [NoZeroDivisors R] (p : ℕ) [CharP R p] (hp : 2 ≤ p) : Nat.Prime p
• CharP.char_prime_of_ne_zero 📋 Mathlib.Algebra.CharP.Defs
  (R : Type u_1) [NonAssocSemiring R] [NoZeroDivisors R] [Nontrivial R] {p : ℕ} [CharP R p] (hp : p ≠ 0) : Nat.Prime p
• CharP.char_is_prime_or_zero 📋 Mathlib.Algebra.CharP.Defs
  (R : Type u_1) [NonAssocSemiring R] [NoZeroDivisors R] [Nontrivial R] (p : ℕ) [hc : CharP R p] : Nat.Prime p ∨ p = 0
• CharP.exists' 📋 Mathlib.Algebra.CharP.Defs
  (R : Type u_2) [NonAssocRing R] [NoZeroDivisors R] [Nontrivial R] : CharZero R ∨ ∃ p, Fact (Nat.Prime p) ∧ CharP R p
• Subalgebra.isSimpleOrder_of_finrank_prime 📋 Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder
  (F : Type u_1) (A : Type u_2) [Field F] [Ring A] [IsDomain A] [Algebra F A] (hp : Nat.Prime (Module.finrank F A)) : IsSimpleOrder (Subalgebra F A)
• CharP.ringChar_of_prime_eq_zero 📋 Mathlib.Algebra.CharP.Basic
  {R : Type u_1} [NonAssocSemiring R] [Nontrivial R] {p : ℕ} (hprime : Nat.Prime p) (hp0 : ↑p = 0) : ringChar R = p
• CharP.charP_iff_prime_eq_zero 📋 Mathlib.Algebra.CharP.Basic
  {R : Type u_1} [NonAssocSemiring R] [Nontrivial R] {p : ℕ} (hp : Nat.Prime p) : CharP R p ↔ ↑p = 0
• CharP.cast_ne_zero_of_ne_of_prime 📋 Mathlib.Algebra.CharP.Basic
  (R : Type u_1) [NonAssocSemiring R] [Nontrivial R] {p q : ℕ} [CharP R p] (hq : Nat.Prime q) (hneq : p ≠ q) : ↑q ≠ 0
• CharZero.charZero_iff_forall_prime_ne_zero 📋 Mathlib.Algebra.CharP.Basic
  (R : Type u_1) [NonAssocRing R] [NoZeroDivisors R] [Nontrivial R] : CharZero R ↔ ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
• Nat.succ_pred_prime 📋 Mathlib.Data.Nat.Prime.Basic
  {p : ℕ} (pp : Nat.Prime p) : p.pred.succ = p
• Nat.coprime_or_dvd_of_prime 📋 Mathlib.Data.Nat.Prime.Basic
  {p : ℕ} (pp : Nat.Prime p) (i : ℕ) : p.Coprime i ∨ p ∣ i
• Nat.Prime.pred_pos 📋 Mathlib.Data.Nat.Prime.Basic
  {p : ℕ} (pp : Nat.Prime p) : 0 < p.pred
• Nat.coprime_primes 📋 Mathlib.Data.Nat.Prime.Basic
  {p q : ℕ} (pp : Nat.Prime p) (pq : Nat.Prime q) : p.Coprime q ↔ p ≠ q
• Nat.Prime.dvd_iff_not_coprime 📋 Mathlib.Data.Nat.Prime.Basic
  {p n : ℕ} (pp : Nat.Prime p) : p ∣ n ↔ ¬p.Coprime n
• Nat.Prime.odd_of_ne_two 📋 Mathlib.Data.Nat.Prime.Basic
  {p : ℕ} (hp : Nat.Prime p) (h_two : p ≠ 2) : Odd p
• Nat.Prime.eq_two_or_odd' 📋 Mathlib.Data.Nat.Prime.Basic
  {p : ℕ} (hp : Nat.Prime p) : p = 2 ∨ Odd p
• Nat.Prime.even_iff 📋 Mathlib.Data.Nat.Prime.Basic
  {p : ℕ} (hp : Nat.Prime p) : Even p ↔ p = 2
• Nat.Prime.odd_iff 📋 Mathlib.Data.Nat.Prime.Basic
  {p : ℕ} (hp : Nat.Prime p) : Odd p ↔ 3 ≤ p
• Nat.eq_one_iff_not_exists_prime_dvd 📋 Mathlib.Data.Nat.Prime.Basic
  {n : ℕ} : n = 1 ↔ ∀ (p : ℕ), Nat.Prime p → ¬p ∣ n
• Nat.coprime_of_lt_prime 📋 Mathlib.Data.Nat.Prime.Basic
  {n p : ℕ} (ne_zero : n ≠ 0) (hlt : n < p) (pp : Nat.Prime p) : p.Coprime n
• Nat.ne_one_iff_exists_prime_dvd 📋 Mathlib.Data.Nat.Prime.Basic
  {n : ℕ} : n ≠ 1 ↔ ∃ p, Nat.Prime p ∧ p ∣ n
• Nat.not_prime_of_dvd_of_ne 📋 Mathlib.Data.Nat.Prime.Basic
  {m n : ℕ} (h1 : m ∣ n) (h2 : m ≠ 1) (h3 : m ≠ n) : ¬Nat.Prime n
• Nat.Prime.dvd_iff_eq 📋 Mathlib.Data.Nat.Prime.Basic
  {p a : ℕ} (hp : Nat.Prime p) (a1 : a ≠ 1) : a ∣ p ↔ p = a
• Nat.forall_prime_of_two_of_odd 📋 Mathlib.Data.Nat.Prime.Basic
  {P : ℕ → Prop} : (P 2 ∧ ∀ (p : ℕ), Nat.Prime p → Odd p → P p) → ∀ (p : ℕ), Nat.Prime p → P p
• Nat.forall_prime_iff_two_and_odd 📋 Mathlib.Data.Nat.Prime.Basic
  {P : ℕ → Prop} : (∀ (p : ℕ), Nat.Prime p → P p) ↔ P 2 ∧ ∀ (p : ℕ), Nat.Prime p → Odd p → P p
• Nat.not_prime_of_dvd_of_lt 📋 Mathlib.Data.Nat.Prime.Basic
  {m n : ℕ} (h1 : m ∣ n) (h2 : 2 ≤ m) (h3 : m < n) : ¬Nat.Prime n
• Nat.Prime.not_coprime_iff_dvd 📋 Mathlib.Data.Nat.Prime.Basic
  {m n : ℕ} : ¬m.Coprime n ↔ ∃ p, Nat.Prime p ∧ p ∣ m ∧ p ∣ n
• Nat.eq_or_coprime_of_le_prime 📋 Mathlib.Data.Nat.Prime.Basic
  {n p : ℕ} (ne_zero : n ≠ 0) (hle : n ≤ p) (pp : Nat.Prime p) : p = n ∨ p.Coprime n
• Nat.Prime.eq_one_of_pow 📋 Mathlib.Data.Nat.Prime.Basic
  {x n : ℕ} (h : Nat.Prime (x ^ n)) : n = 1
• Nat.Prime.not_prime_pow' 📋 Mathlib.Data.Nat.Prime.Basic
  {x n : ℕ} (hn : n ≠ 1) : ¬Nat.Prime (x ^ n)
• Nat.coprime_of_dvd' 📋 Mathlib.Data.Nat.Prime.Basic
  {m n : ℕ} (H : ∀ (k : ℕ), Nat.Prime k → k ∣ m → k ∣ n → k ∣ 1) : m.Coprime n
• Nat.Prime.coprime_pow_of_not_dvd 📋 Mathlib.Data.Nat.Prime.Basic
  {p m a : ℕ} (pp : Nat.Prime p) (h : ¬p ∣ a) : a.Coprime (p ^ m)
• Nat.Prime.even_sub_one 📋 Mathlib.Data.Nat.Prime.Basic
  {p : ℕ} (hp : Nat.Prime p) (h2 : p ≠ 2) : Even (p - 1)
• Nat.Prime.not_prime_pow 📋 Mathlib.Data.Nat.Prime.Basic
  {x n : ℕ} (hn : 2 ≤ n) : ¬Nat.Prime (x ^ n)
• Nat.dvd_of_forall_prime_mul_dvd 📋 Mathlib.Data.Nat.Prime.Basic
  {a b : ℕ} (hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ a → p * a ∣ b) : a ∣ b
• Nat.Prime.dvd_of_dvd_pow 📋 Mathlib.Data.Nat.Prime.Basic
  {p m n : ℕ} (pp : Nat.Prime p) (h : p ∣ m ^ n) : p ∣ m
• Nat.Prime.five_le_of_ne_two_of_ne_three 📋 Mathlib.Data.Nat.Prime.Basic
  {p : ℕ} (hp : Nat.Prime p) (h_two : p ≠ 2) (h_three : p ≠ 3) : 5 ≤ p
• Nat.not_prime_mul 📋 Mathlib.Data.Nat.Prime.Basic
  {a b : ℕ} (a1 : a ≠ 1) (b1 : b ≠ 1) : ¬Nat.Prime (a * b)
• Nat.prime_eq_prime_of_dvd_pow 📋 Mathlib.Data.Nat.Prime.Basic
  {m p q : ℕ} (pp : Nat.Prime p) (pq : Nat.Prime q) (h : p ∣ q ^ m) : p = q
• Nat.Prime.not_dvd_mul 📋 Mathlib.Data.Nat.Prime.Basic
  {p m n : ℕ} (pp : Nat.Prime p) (Hm : ¬p ∣ m) (Hn : ¬p ∣ n) : ¬p ∣ m * n
• Nat.Prime.eq_two_or_odd 📋 Mathlib.Data.Nat.Prime.Basic
  {p : ℕ} (hp : Nat.Prime p) : p = 2 ∨ p % 2 = 1
• Nat.Prime.mod_two_eq_one_iff_ne_two 📋 Mathlib.Data.Nat.Prime.Basic
  {p : ℕ} (hp : Nat.Prime p) : p % 2 = 1 ↔ p ≠ 2
• Nat.not_prime_of_mul_eq 📋 Mathlib.Data.Nat.Prime.Basic
  {a b n : ℕ} (h : a * b = n) (h₁ : a ≠ 1) (h₂ : b ≠ 1) : ¬Nat.Prime n
• Nat.Prime.dvd_mul_of_dvd_ne 📋 Mathlib.Data.Nat.Prime.Basic
  {p1 p2 n : ℕ} (h_ne : p1 ≠ p2) (pp1 : Nat.Prime p1) (pp2 : Nat.Prime p2) (h1 : p1 ∣ n) (h2 : p2 ∣ n) : p1 * p2 ∣ n
• Nat.exists_dvd_of_not_prime 📋 Mathlib.Data.Nat.Prime.Basic
  {n : ℕ} (n2 : 2 ≤ n) (np : ¬Nat.Prime n) : ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n
• Nat.not_prime_iff_exists_dvd_ne 📋 Mathlib.Data.Nat.Prime.Basic
  {n : ℕ} (h : 2 ≤ n) : ¬Nat.Prime n ↔ ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n
• Nat.prime_mul_iff 📋 Mathlib.Data.Nat.Prime.Basic
  {a b : ℕ} : Nat.Prime (a * b) ↔ Nat.Prime a ∧ b = 1 ∨ Nat.Prime b ∧ a = 1
• Nat.Prime.pow_eq_iff 📋 Mathlib.Data.Nat.Prime.Basic
  {p a k : ℕ} (hp : Nat.Prime p) : a ^ k = p ↔ a = p ∧ k = 1
• Nat.exists_dvd_of_not_prime2 📋 Mathlib.Data.Nat.Prime.Basic
  {n : ℕ} (n2 : 2 ≤ n) (np : ¬Nat.Prime n) : ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n
• Nat.not_prime_iff_exists_dvd_lt 📋 Mathlib.Data.Nat.Prime.Basic
  {n : ℕ} (h : 2 ≤ n) : ¬Nat.Prime n ↔ ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n
• Nat.coprime_pow_primes 📋 Mathlib.Data.Nat.Prime.Basic
  {p q : ℕ} (n m : ℕ) (pp : Nat.Prime p) (pq : Nat.Prime q) (h : p ≠ q) : (p ^ n).Coprime (q ^ m)
• Nat.not_prime_iff_exists_mul_eq 📋 Mathlib.Data.Nat.Prime.Basic
  {n : ℕ} (h : 2 ≤ n) : ¬Nat.Prime n ↔ ∃ a b, a < n ∧ b < n ∧ a * b = n
• Nat.dvd_prime_pow 📋 Mathlib.Data.Nat.Prime.Basic
  {p : ℕ} (pp : Nat.Prime p) {m i : ℕ} : i ∣ p ^ m ↔ ∃ k ≤ m, i = p ^ k
• Nat.Prime.mul_eq_prime_sq_iff 📋 Mathlib.Data.Nat.Prime.Basic
  {x y p : ℕ} (hp : Nat.Prime p) (hx : x ≠ 1) (hy : y ≠ 1) : x * y = p ^ 2 ↔ x = p ∧ y = p
• Nat.eq_prime_pow_of_dvd_least_prime_pow 📋 Mathlib.Data.Nat.Prime.Basic
  {a p k : ℕ} (pp : Nat.Prime p) (h₁ : ¬a ∣ p ^ k) (h₂ : a ∣ p ^ (k + 1)) : a = p ^ (k + 1)
• Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul 📋 Mathlib.Data.Nat.Prime.Basic
  {p : ℕ} (p_prime : Nat.Prime p) {m n k l : ℕ} (hpm : p ^ k ∣ m) (hpn : p ^ l ∣ n) (hpmn : p ^ (k + l + 1) ∣ m * n) : p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
• Function.minimalPeriod_eq_prime 📋 Mathlib.Dynamics.PeriodicPts.Lemmas
  {α : Type u_1} {f : α → α} {x : α} {p : ℕ} [hp : Fact (Nat.Prime p)] (hper : Function.IsPeriodicPt f p x) (hfix : ¬Function.IsFixedPt f x) : Function.minimalPeriod f x = p
• Function.minimalPeriod_eq_prime_iff 📋 Mathlib.Dynamics.PeriodicPts.Lemmas
  {α : Type u_1} {f : α → α} {x : α} {p : ℕ} [hp : Fact (Nat.Prime p)] : Function.minimalPeriod f x = p ↔ Function.IsPeriodicPt f p x ∧ ¬Function.IsFixedPt f x
• Function.minimalPeriod_eq_prime_pow 📋 Mathlib.Dynamics.PeriodicPts.Lemmas
  {α : Type u_1} {f : α → α} {x : α} {p k : ℕ} [hp : Fact (Nat.Prime p)] (hk : ¬Function.IsPeriodicPt f (p ^ k) x) (hk1 : Function.IsPeriodicPt f (p ^ (k + 1)) x) : Function.minimalPeriod f x = p ^ (k + 1)
• Nat.Prime.pow_minFac 📋 Mathlib.Data.Nat.Prime.Pow
  {p k : ℕ} (hp : Nat.Prime p) (hk : k ≠ 0) : (p ^ k).minFac = p
• Nat.Prime.isPrimePow 📋 Mathlib.Algebra.IsPrimePow
  {p : ℕ} (hp : Nat.Prime p) : IsPrimePow p
• isPrimePow_nat_iff 📋 Mathlib.Algebra.IsPrimePow
  (n : ℕ) : IsPrimePow n ↔ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
• isPrimePow_nat_iff_bounded 📋 Mathlib.Algebra.IsPrimePow
  (n : ℕ) : IsPrimePow n ↔ ∃ p ≤ n, ∃ k ≤ n, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
• isPrimePow_nat_iff_bounded_log 📋 Mathlib.Algebra.IsPrimePow
  (n : ℕ) : IsPrimePow n ↔ ∃ k ≤ Nat.log 2 n, 0 < k ∧ ∃ p ≤ n, n = p ^ k ∧ Nat.Prime p
• Nat.primeFactorsList_prime 📋 Mathlib.Data.Nat.Factors
  {p : ℕ} (hp : Nat.Prime p) : p.primeFactorsList = [p]
• Nat.prime_of_mem_primeFactorsList 📋 Mathlib.Data.Nat.Factors
  {n p : ℕ} : p ∈ n.primeFactorsList → Nat.Prime p
• Nat.Prime.primeFactorsList_pow 📋 Mathlib.Data.Nat.Factors
  {p : ℕ} (hp : Nat.Prime p) (n : ℕ) : (p ^ n).primeFactorsList = List.replicate n p
• Nat.mem_primeFactorsList_iff_dvd 📋 Mathlib.Data.Nat.Factors
  {n p : ℕ} (hn : n ≠ 0) (hp : Nat.Prime p) : p ∈ n.primeFactorsList ↔ p ∣ n
• Nat.primeFactorsList_unique 📋 Mathlib.Data.Nat.Factors
  {n : ℕ} {l : List ℕ} (h₁ : l.prod = n) (h₂ : ∀ p ∈ l, Nat.Prime p) : l.Perm n.primeFactorsList
• Nat.mem_primeFactorsList 📋 Mathlib.Data.Nat.Factors
  {n p : ℕ} (hn : n ≠ 0) : p ∈ n.primeFactorsList ↔ Nat.Prime p ∧ p ∣ n
• Nat.isChain_cons_primeFactorsList 📋 Mathlib.Data.Nat.Factors
  {n a : ℕ} : (∀ (p : ℕ), Nat.Prime p → p ∣ n → a ≤ p) → List.IsChain (fun x1 x2 => x1 ≤ x2) (a :: n.primeFactorsList)
• Nat.mem_primeFactorsList' 📋 Mathlib.Data.Nat.Factors
  {n p : ℕ} : p ∈ n.primeFactorsList ↔ Nat.Prime p ∧ p ∣ n ∧ n ≠ 0
• Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt 📋 Mathlib.Data.Nat.Factors
  {n : ℕ} (n2 : 2 < n) : 4 ∣ n ∨ ∃ p, Nat.Prime p ∧ p ∣ n ∧ Odd p
• Nat.replicate_subperm_primeFactorsList_iff 📋 Mathlib.Data.Nat.Factors
  {a b n : ℕ} (ha : Nat.Prime a) (hb : b ≠ 0) : (List.replicate n a).Subperm b.primeFactorsList ↔ a ^ n ∣ b
• Nat.eq_prime_pow_of_unique_prime_dvd 📋 Mathlib.Data.Nat.Factors
  {n p : ℕ} (hpos : n ≠ 0) (h : ∀ {d : ℕ}, Nat.Prime d → d ∣ n → d = p) : n = p ^ n.primeFactorsList.length
• Nat.eq_two_pow_or_exists_odd_prime_and_dvd 📋 Mathlib.Data.Nat.Factors
  (n : ℕ) : (∃ k, n = 2 ^ k) ∨ ∃ p, Nat.Prime p ∧ p ∣ n ∧ Odd p
• Nat.not_bddAbove_setOfPred_prime 📋 Mathlib.Data.Nat.Prime.Infinite
  : ¬BddAbove {p | Nat.Prime p}
• Nat.not_bddAbove_setOf_prime 📋 Mathlib.Data.Nat.Prime.Infinite
  : ¬BddAbove {p | Nat.Prime p}
• Nat.exists_infinite_primes 📋 Mathlib.Data.Nat.Prime.Infinite
  (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p
• Nat.infinite_setOfPred_prime 📋 Mathlib.Data.Nat.PrimeFin
  : {p | Nat.Prime p}.Infinite
• Nat.infinite_setOf_prime 📋 Mathlib.Data.Nat.PrimeFin
  : {p | Nat.Prime p}.Infinite
• Nat.Prime.primeFactors 📋 Mathlib.Data.Nat.PrimeFin
  {p : ℕ} (hp : Nat.Prime p) : p.primeFactors = {p}
• Nat.Prime.mem_primeFactors_self 📋 Mathlib.Data.Nat.PrimeFin
  {p : ℕ} (hp : Nat.Prime p) : p ∈ p.primeFactors
• Nat.prime_of_mem_primeFactors 📋 Mathlib.Data.Nat.PrimeFin
  {n p : ℕ} (hp : p ∈ n.primeFactors) : Nat.Prime p
• Nat.Prime.mem_primeFactors' 📋 Mathlib.Data.Nat.PrimeFin
  {n p : ℕ} (hp : Nat.Prime p) (hdvd : p ∣ n) [NeZero n] : p ∈ n.primeFactors
• Nat.Prime.mem_primeFactors 📋 Mathlib.Data.Nat.PrimeFin
  {n p : ℕ} (hp : Nat.Prime p) (hdvd : p ∣ n) (hn : n ≠ 0) : p ∈ n.primeFactors
• Nat.mem_primeFactors_of_ne_zero 📋 Mathlib.Data.Nat.PrimeFin
  {n p : ℕ} (hn : n ≠ 0) : p ∈ n.primeFactors ↔ Nat.Prime p ∧ p ∣ n
• Nat.mem_primeFactors 📋 Mathlib.Data.Nat.PrimeFin
  {n p : ℕ} : p ∈ n.primeFactors ↔ Nat.Prime p ∧ p ∣ n ∧ n ≠ 0
• Nat.primeFactors_prime_pow 📋 Mathlib.Data.Nat.PrimeFin
  {k p : ℕ} (hk : k ≠ 0) (hp : Nat.Prime p) : (p ^ k).primeFactors = {p}
• Nat.primeFactors_eq_to_filter_divisors_prime 📋 Mathlib.NumberTheory.Divisors
  (n : ℕ) : n.primeFactors = {p ∈ n.divisors | Nat.Prime p}
• Nat.sum_properDivisors_eq_one_iff_prime 📋 Mathlib.NumberTheory.Divisors
  {n : ℕ} : ∑ x ∈ n.properDivisors, x = 1 ↔ Nat.Prime n
• Nat.Prime.properDivisors 📋 Mathlib.NumberTheory.Divisors
  {p : ℕ} (pp : Nat.Prime p) : p.properDivisors = {1}
• Nat.properDivisors_eq_singleton_one_iff_prime 📋 Mathlib.NumberTheory.Divisors
  {n : ℕ} : n.properDivisors = {1} ↔ Nat.Prime n
• Nat.Prime.prod_properDivisors 📋 Mathlib.NumberTheory.Divisors
  {α : Type u_1} [CommMonoid α] {p : ℕ} {f : ℕ → α} (h : Nat.Prime p) : ∏ x ∈ p.properDivisors, f x = f 1
• Nat.Prime.sum_properDivisors 📋 Mathlib.NumberTheory.Divisors
  {α : Type u_1} [AddCommMonoid α] {p : ℕ} {f : ℕ → α} (h : Nat.Prime p) : ∑ x ∈ p.properDivisors, f x = f 1
• Nat.Prime.divisors 📋 Mathlib.NumberTheory.Divisors
  {p : ℕ} (pp : Nat.Prime p) : p.divisors = {1, p}
• Nat.Prime.prod_divisors 📋 Mathlib.NumberTheory.Divisors
  {α : Type u_1} [CommMonoid α] {p : ℕ} {f : ℕ → α} (h : Nat.Prime p) : ∏ x ∈ p.divisors, f x = f p * f 1
• Nat.Prime.sum_divisors 📋 Mathlib.NumberTheory.Divisors
  {α : Type u_1} [AddCommMonoid α] {p : ℕ} {f : ℕ → α} (h : Nat.Prime p) : ∑ x ∈ p.divisors, f x = f p + f 1
• Nat.properDivisors_prime_pow 📋 Mathlib.NumberTheory.Divisors
  {p : ℕ} (pp : Nat.Prime p) (k : ℕ) : (p ^ k).properDivisors = Finset.map { toFun := fun x => p ^ x, inj' := ⋯ } (Finset.range k)
• Nat.prod_properDivisors_prime_pow 📋 Mathlib.NumberTheory.Divisors
  {α : Type u_1} [CommMonoid α] {k p : ℕ} {f : ℕ → α} (h : Nat.Prime p) : ∏ x ∈ (p ^ k).properDivisors, f x = ∏ x ∈ Finset.range k, f (p ^ x)
• Nat.sum_properDivisors_prime_nsmul 📋 Mathlib.NumberTheory.Divisors
  {α : Type u_1} [AddCommMonoid α] {k p : ℕ} {f : ℕ → α} (h : Nat.Prime p) : ∑ x ∈ (p ^ k).properDivisors, f x = ∑ x ∈ Finset.range k, f (p ^ x)
• Nat.mem_divisors_prime_pow 📋 Mathlib.NumberTheory.Divisors
  {p : ℕ} (pp : Nat.Prime p) (k : ℕ) {x : ℕ} : x ∈ (p ^ k).divisors ↔ ∃ j ≤ k, x = p ^ j
• Nat.divisors_prime_pow 📋 Mathlib.NumberTheory.Divisors
  {p : ℕ} (pp : Nat.Prime p) (k : ℕ) : (p ^ k).divisors = Finset.map { toFun := fun x => p ^ x, inj' := ⋯ } (Finset.range (k + 1))
• Nat.mem_properDivisors_prime_pow 📋 Mathlib.NumberTheory.Divisors
  {p : ℕ} (pp : Nat.Prime p) (k : ℕ) {x : ℕ} : x ∈ (p ^ k).properDivisors ↔ ∃ j, ∃ (_ : j < k), x = p ^ j
• Nat.prod_divisors_prime_pow 📋 Mathlib.NumberTheory.Divisors
  {α : Type u_1} [CommMonoid α] {k p : ℕ} {f : ℕ → α} (h : Nat.Prime p) : ∏ x ∈ (p ^ k).divisors, f x = ∏ x ∈ Finset.range (k + 1), f (p ^ x)
• Nat.sum_divisors_prime_pow 📋 Mathlib.NumberTheory.Divisors
  {α : Type u_1} [AddCommMonoid α] {k p : ℕ} {f : ℕ → α} (h : Nat.Prime p) : ∑ x ∈ (p ^ k).divisors, f x = ∑ x ∈ Finset.range (k + 1), f (p ^ x)
• addOrderOf_eq_prime 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [AddMonoid G] {x : G} {p : ℕ} [hp : Fact (Nat.Prime p)] (hg : p • x = 0) (hg1 : x ≠ 0) : addOrderOf x = p
• orderOf_eq_prime 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [Monoid G] {x : G} {p : ℕ} [hp : Fact (Nat.Prime p)] (hg : x ^ p = 1) (hg1 : x ≠ 1) : orderOf x = p
• addOrderOf_eq_prime_iff 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [AddMonoid G] {x : G} {p : ℕ} [hp : Fact (Nat.Prime p)] : addOrderOf x = p ↔ p • x = 0 ∧ x ≠ 0
• orderOf_eq_prime_iff 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [Monoid G] {x : G} {p : ℕ} [hp : Fact (Nat.Prime p)] : orderOf x = p ↔ x ^ p = 1 ∧ x ≠ 1
• AddCommute.addOrderOf_add_eq_left_of_forall_prime_mul_dvd 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [AddMonoid G] {x y : G} (h : AddCommute x y) (hx : IsOfFinAddOrder x) (hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ addOrderOf y → p * addOrderOf y ∣ addOrderOf x) : addOrderOf (x + y) = addOrderOf x
• AddCommute.addOrderOf_add_eq_right_of_forall_prime_mul_dvd 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [AddMonoid G] {x y : G} (h : AddCommute x y) (hy : IsOfFinAddOrder y) (hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ addOrderOf x → p * addOrderOf x ∣ addOrderOf y) : addOrderOf (x + y) = addOrderOf y
• Commute.orderOf_mul_eq_left_of_forall_prime_mul_dvd 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [Monoid G] {x y : G} (h : Commute x y) (hx : IsOfFinOrder x) (hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf y → p * orderOf y ∣ orderOf x) : orderOf (x * y) = orderOf x
• Commute.orderOf_mul_eq_right_of_forall_prime_mul_dvd 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [Monoid G] {x y : G} (h : Commute x y) (hy : IsOfFinOrder y) (hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y) : orderOf (x * y) = orderOf y
• exists_addOrderOf_eq_prime_pow_iff 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [AddMonoid G] {x : G} {p : ℕ} [hp : Fact (Nat.Prime p)] : (∃ k, addOrderOf x = p ^ k) ↔ ∃ m, p ^ m • x = 0
• exists_orderOf_eq_prime_pow_iff 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [Monoid G] {x : G} {p : ℕ} [hp : Fact (Nat.Prime p)] : (∃ k, orderOf x = p ^ k) ↔ ∃ m, x ^ p ^ m = 1
• addOrderOf_eq_of_nsmul_and_div_prime_nsmul 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [AddMonoid G] {x : G} {n : ℕ} (hn : 0 < n) (hx : n • x = 0) (hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → (n / p) • x ≠ 0) : addOrderOf x = n
• orderOf_eq_of_pow_and_pow_div_prime 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [Monoid G] {x : G} {n : ℕ} (hn : 0 < n) (hx : x ^ n = 1) (hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1) : orderOf x = n
• charP_of_prime_pow_injective 📋 Mathlib.GroupTheory.OrderOfElement
  (R : Type u_6) [Ring R] [Fintype R] (p n : ℕ) [hp : Fact (Nat.Prime p)] (hn : Fintype.card R = p ^ n) (hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n) : CharP R (p ^ n)
• addOrderOf_eq_prime_pow 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [AddMonoid G] {x : G} {n p : ℕ} [hp : Fact (Nat.Prime p)] (hnot : ¬p ^ n • x = 0) (hfin : p ^ (n + 1) • x = 0) : addOrderOf x = p ^ (n + 1)
• orderOf_eq_prime_pow 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [Monoid G] {x : G} {n p : ℕ} [hp : Fact (Nat.Prime p)] (hnot : ¬x ^ p ^ n = 1) (hfin : x ^ p ^ (n + 1) = 1) : orderOf x = p ^ (n + 1)
• ZMod.isUnit_prime_of_not_dvd 📋 Mathlib.Data.ZMod.Basic
  {n p : ℕ} (hp : Nat.Prime p) (h : ¬p ∣ n) : IsUnit ↑p
• ZMod.isUnit_prime_iff_not_dvd 📋 Mathlib.Data.ZMod.Basic
  {n p : ℕ} (hp : Nat.Prime p) : IsUnit ↑p ↔ ¬p ∣ n
• ZMod.ringEquivOfPrime 📋 Mathlib.Data.ZMod.Basic
  (R : Type u_1) [Ring R] [Fintype R] {p : ℕ} (hp : Nat.Prime p) (hR : Fintype.card R = p) : ZMod p ≃+* R
• ZMod.ringEquivOfPrime_eq_ringEquiv 📋 Mathlib.Data.ZMod.Basic
  (R : Type u_1) [Ring R] [Fintype R] {p : ℕ} [CharP R p] (hp : Nat.Prime p) (hR : Fintype.card R = p) : ZMod.ringEquivOfPrime R hp hR = ZMod.ringEquiv R hR
• ZMod.prime_natCast_not_isUnit_pow 📋 Mathlib.Data.ZMod.Basic
  {p d : ℕ} (hp : Nat.Prime p) (hd : 0 < d) : ¬IsUnit ↑p
• ZMod.isUnit_natCast_iff_not_dvd_pow 📋 Mathlib.Data.ZMod.Basic
  {p d a : ℕ} (hp : Nat.Prime p) (hd : 0 < d) : IsUnit ↑a ↔ ¬p ∣ a
• padicValNat_def 📋 Mathlib.NumberTheory.Padics.PadicVal.Defs
  {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : n ≠ 0) : padicValNat p n = multiplicity p n
• padicValNat_eq_emultiplicity 📋 Mathlib.NumberTheory.Padics.PadicVal.Defs
  {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : n ≠ 0) : ↑(padicValNat p n) = emultiplicity p n
• padicValNat.maxPowDiv_eq_emultiplicity 📋 Mathlib.NumberTheory.Padics.PadicVal.Defs
  {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : n ≠ 0) : ↑(padicValNat p n) = emultiplicity p n
• le_padicValNat_iff_replicate_subperm_primeFactorsList 📋 Mathlib.NumberTheory.Padics.PadicVal.Defs
  {a b n : ℕ} (ha : Nat.Prime a) (hb : b ≠ 0) : n ≤ padicValNat a b ↔ (List.replicate n a).Subperm b.primeFactorsList
• le_emultiplicity_iff_replicate_subperm_primeFactorsList 📋 Mathlib.NumberTheory.Padics.PadicVal.Defs
  {a b n : ℕ} (ha : Nat.Prime a) (hb : b ≠ 0) : ↑n ≤ emultiplicity a b ↔ (List.replicate n a).Subperm b.primeFactorsList
• Nat.Prime.factorization 📋 Mathlib.Data.Nat.Factorization.Defs
  {p : ℕ} (hp : Nat.Prime p) : p.factorization = fun₀ | p => 1
• Nat.factorization_def 📋 Mathlib.Data.Nat.Factorization.Defs
  (n : ℕ) {p : ℕ} (pp : Nat.Prime p) : n.factorization p = padicValNat p n
• Nat.factorization_eq_zero_of_not_prime 📋 Mathlib.Data.Nat.Factorization.Defs
  (n : ℕ) {p : ℕ} (hp : ¬Nat.Prime p) : n.factorization p = 0
• Nat.isSquare_iff_even_factorization 📋 Mathlib.Data.Nat.Factorization.Defs
  {n : ℕ} : IsSquare n ↔ ∀ (p : ℕ), Nat.Prime p → Even (n.factorization p)
• Nat.Prime.factorization_pow 📋 Mathlib.Data.Nat.Factorization.Defs
  {p k : ℕ} (hp : Nat.Prime p) : (p ^ k).factorization = fun₀ | p => k
• Nat.factorizationEquiv 📋 Mathlib.Data.Nat.Factorization.Defs
  : ℕ+ ≃ { f // ∀ p ∈ f.support, Nat.Prime p }
• Nat.multiplicity_eq_factorization 📋 Mathlib.Data.Nat.Factorization.Defs
  {n p : ℕ} (pp : Nat.Prime p) (hn : n ≠ 0) : multiplicity p n = n.factorization p
• Int.isSquare_iff_nonneg_even_factorization 📋 Mathlib.Data.Nat.Factorization.Defs
  {n : ℤ} : IsSquare n ↔ 0 ≤ n ∧ ∀ (p : ℕ), Nat.Prime p → Even (n.natAbs.factorization p)
• Nat.Prime.factorization_pos_of_dvd 📋 Mathlib.Data.Nat.Factorization.Defs
  {n p : ℕ} (hp : Nat.Prime p) (hn : n ≠ 0) (h : p ∣ n) : 0 < n.factorization p
• Nat.factorization_eq_zero_iff 📋 Mathlib.Data.Nat.Factorization.Defs
  (n p : ℕ) : n.factorization p = 0 ↔ ¬Nat.Prime p ∨ ¬p ∣ n ∨ n = 0
• Nat.pow_succ_factorization_not_dvd 📋 Mathlib.Data.Nat.Factorization.Defs
  {n p : ℕ} (hn : n ≠ 0) (hp : Nat.Prime p) : ¬p ^ (n.factorization p + 1) ∣ n

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. 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.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

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. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c