Loogle!

Result

Found 20288 declarations mentioning HMul.hMul. Of these, 20235 match your pattern(s). Of these, only the first 200 are shown.

• Nat.mul_pos 📋 Init.Prelude
  {n m : ℕ} (hn : 0 < n) (hm : 0 < m) : 0 < n * m
• instNeZeroNatHMul 📋 Init.Data.NeZero
  {n m : ℕ} [hn : NeZero n] [hm : NeZero m] : NeZero (n * m)
• Nat.instAssociativeHMul 📋 Init.Data.Nat.Basic
  : Std.Associative fun x1 x2 => x1 * x2
• Nat.instCommutativeHMul 📋 Init.Data.Nat.Basic
  : Std.Commutative fun x1 x2 => x1 * x2
• Nat.mul_one 📋 Init.Data.Nat.Basic
  (n : ℕ) : n * 1 = n
• Nat.one_mul 📋 Init.Data.Nat.Basic
  (n : ℕ) : 1 * n = n
• Nat.instLawfulIdentityHMulOfNat 📋 Init.Data.Nat.Basic
  : Std.LawfulIdentity (fun x1 x2 => x1 * x2) 1
• Nat.mul_eq 📋 Init.Data.Nat.Basic
  {x y : ℕ} : x.mul y = x * y
• Nat.mul_zero 📋 Init.Data.Nat.Basic
  (n : ℕ) : n * 0 = 0
• Nat.zero_mul 📋 Init.Data.Nat.Basic
  (n : ℕ) : 0 * n = 0
• Nat.mul_comm 📋 Init.Data.Nat.Basic
  (n m : ℕ) : n * m = m * n
• Nat.mul_two 📋 Init.Data.Nat.Basic
  (n : ℕ) : n * 2 = n + n
• Nat.two_mul 📋 Init.Data.Nat.Basic
  (n : ℕ) : 2 * n = n + n
• Nat.mul_le_mul_left 📋 Init.Data.Nat.Basic
  {n m : ℕ} (k : ℕ) (h : n ≤ m) : k * n ≤ k * m
• Nat.mul_le_mul_right 📋 Init.Data.Nat.Basic
  {n m : ℕ} (k : ℕ) (h : n ≤ m) : n * k ≤ m * k
• Nat.mul_pred 📋 Init.Data.Nat.Basic
  (n m : ℕ) : n * m.pred = n * m - n
• Nat.mul_succ 📋 Init.Data.Nat.Basic
  (n m : ℕ) : n * m.succ = n * m + n
• Nat.pred_mul 📋 Init.Data.Nat.Basic
  (n m : ℕ) : n.pred * m = n * m - m
• Nat.succ_mul 📋 Init.Data.Nat.Basic
  (n m : ℕ) : n.succ * m = n * m + m
• Nat.mul_le_mul 📋 Init.Data.Nat.Basic
  {n₁ m₁ n₂ m₂ : ℕ} (h₁ : n₁ ≤ n₂) (h₂ : m₁ ≤ m₂) : n₁ * m₁ ≤ n₂ * m₂
• Nat.eq_of_mul_eq_mul_left 📋 Init.Data.Nat.Basic
  {m k n : ℕ} (hn : 0 < n) (h : n * m = n * k) : m = k
• Nat.eq_of_mul_eq_mul_right 📋 Init.Data.Nat.Basic
  {n m k : ℕ} (hm : 0 < m) (h : n * m = k * m) : n = k
• Nat.pow_succ 📋 Init.Data.Nat.Basic
  (n m : ℕ) : n ^ m.succ = n ^ m * n
• Nat.le_of_mul_le_mul_left 📋 Init.Data.Nat.Basic
  {a b c : ℕ} (h : c * a ≤ c * b) (hc : 0 < c) : a ≤ b
• Nat.le_of_mul_le_mul_right 📋 Init.Data.Nat.Basic
  {a b c : ℕ} (h : a * c ≤ b * c) (hc : 0 < c) : a ≤ b
• Nat.mul_lt_mul_of_pos_left 📋 Init.Data.Nat.Basic
  {n m k : ℕ} (h : n < m) (hk : k > 0) : k * n < k * m
• Nat.mul_lt_mul_of_pos_right 📋 Init.Data.Nat.Basic
  {n m k : ℕ} (h : n < m) (hk : k > 0) : n * k < m * k
• Nat.mul_assoc 📋 Init.Data.Nat.Basic
  (n m k : ℕ) : n * m * k = n * (m * k)
• Nat.mul_le_mul_left_iff 📋 Init.Data.Nat.Basic
  {n m k : ℕ} (w : 0 < k) : k * n ≤ k * m ↔ n ≤ m
• Nat.mul_le_mul_right_iff 📋 Init.Data.Nat.Basic
  {n m k : ℕ} (w : 0 < k) : n * k ≤ m * k ↔ n ≤ m
• Nat.mul_left_comm 📋 Init.Data.Nat.Basic
  (n m k : ℕ) : n * (m * k) = m * (n * k)
• Nat.add_one_mul 📋 Init.Data.Nat.Basic
  (n m : ℕ) : (n + 1) * m = n * m + m
• Nat.mul_add_one 📋 Init.Data.Nat.Basic
  (n m : ℕ) : n * (m + 1) = n * m + n
• Nat.mul_sub_one 📋 Init.Data.Nat.Basic
  (n m : ℕ) : n * (m - 1) = n * m - n
• Nat.sub_one_mul 📋 Init.Data.Nat.Basic
  (n m : ℕ) : (n - 1) * m = n * m - m
• Nat.add_mul 📋 Init.Data.Nat.Basic
  (n m k : ℕ) : (n + m) * k = n * k + m * k
• Nat.left_distrib 📋 Init.Data.Nat.Basic
  (n m k : ℕ) : n * (m + k) = n * m + n * k
• Nat.mul_add 📋 Init.Data.Nat.Basic
  (n m k : ℕ) : n * (m + k) = n * m + n * k
• Nat.mul_sub 📋 Init.Data.Nat.Basic
  (n m k : ℕ) : n * (m - k) = n * m - n * k
• Nat.mul_sub_left_distrib 📋 Init.Data.Nat.Basic
  (n m k : ℕ) : n * (m - k) = n * m - n * k
• Nat.mul_sub_right_distrib 📋 Init.Data.Nat.Basic
  (n m k : ℕ) : (n - m) * k = n * k - m * k
• Nat.right_distrib 📋 Init.Data.Nat.Basic
  (n m k : ℕ) : (n + m) * k = n * k + m * k
• Nat.sub_mul 📋 Init.Data.Nat.Basic
  (n m k : ℕ) : (n - m) * k = n * k - m * k
• Nat.pow_add_one 📋 Init.Data.Nat.Basic
  (n m : ℕ) : n ^ (m + 1) = n ^ m * n
• Nat.mul_pow 📋 Init.Data.Nat.Basic
  (a b n : ℕ) : (a * b) ^ n = a ^ n * b ^ n
• Nat.div_mul_le_self 📋 Init.Data.Nat.Div.Basic
  (m n : ℕ) : m / n * n ≤ m
• Nat.mul_div_le 📋 Init.Data.Nat.Div.Basic
  (m n : ℕ) : n * (m / n) ≤ m
• Nat.mul_mod_left 📋 Init.Data.Nat.Div.Basic
  (m n : ℕ) : m * n % n = 0
• Nat.mul_mod_right 📋 Init.Data.Nat.Div.Basic
  (m n : ℕ) : m * n % m = 0
• Nat.div_le_of_le_mul 📋 Init.Data.Nat.Div.Basic
  {m n k : ℕ} : m ≤ k * n → m / k ≤ n
• Nat.mul_div_cancel 📋 Init.Data.Nat.Div.Basic
  (m : ℕ) {n : ℕ} (H : 0 < n) : m * n / n = m
• Nat.mul_div_cancel_left 📋 Init.Data.Nat.Div.Basic
  (m : ℕ) {n : ℕ} (H : 0 < n) : n * m / n = m
• Nat.mul_div_left 📋 Init.Data.Nat.Div.Basic
  (m : ℕ) {n : ℕ} (H : 0 < n) : m * n / n = m
• Nat.mul_div_right 📋 Init.Data.Nat.Div.Basic
  (n : ℕ) {m : ℕ} (H : 0 < m) : m * n / m = n
• Nat.div_eq_of_eq_mul_left 📋 Init.Data.Nat.Div.Basic
  {n m k : ℕ} (H1 : 0 < n) (H2 : m = k * n) : m / n = k
• Nat.div_eq_of_eq_mul_right 📋 Init.Data.Nat.Div.Basic
  {n m k : ℕ} (H1 : 0 < n) (H2 : m = n * k) : m / n = k
• Nat.div_add_mod 📋 Init.Data.Nat.Div.Basic
  (m n : ℕ) : n * (m / n) + m % n = m
• Nat.mod_add_div 📋 Init.Data.Nat.Div.Basic
  (m k : ℕ) : m % k + k * (m / k) = m
• Nat.mod_def 📋 Init.Data.Nat.Div.Basic
  (m k : ℕ) : m % k = m - k * (m / k)
• Nat.mod_eq_sub_div_mul 📋 Init.Data.Nat.Div.Basic
  {x k : ℕ} : x % k = x - x / k * k
• Nat.mod_eq_sub_mul_div 📋 Init.Data.Nat.Div.Basic
  {x k : ℕ} : x % k = x - k * (x / k)
• Nat.add_mul_mod_self_left 📋 Init.Data.Nat.Div.Basic
  (x y z : ℕ) : (x + y * z) % y = x % y
• Nat.add_mul_mod_self_right 📋 Init.Data.Nat.Div.Basic
  (x y z : ℕ) : (x + y * z) % z = x % z
• Nat.div_div_eq_div_mul 📋 Init.Data.Nat.Div.Basic
  (m n k : ℕ) : m / n / k = m / (n * k)
• Nat.div_lt_iff_lt_mul 📋 Init.Data.Nat.Div.Basic
  {k x y : ℕ} (Hk : 0 < k) : x / k < y ↔ x < y * k
• Nat.le_div_iff_mul_le 📋 Init.Data.Nat.Div.Basic
  {k x y : ℕ} (k0 : 0 < k) : x ≤ y / k ↔ x * k ≤ y
• Nat.mul_add_mod_self_left 📋 Init.Data.Nat.Div.Basic
  (a b c : ℕ) : (a * b + c) % a = c % a
• Nat.mul_add_mod_self_right 📋 Init.Data.Nat.Div.Basic
  (a b c : ℕ) : (a * b + c) % b = c % b
• Nat.mul_mod_mul_left 📋 Init.Data.Nat.Div.Basic
  (z x y : ℕ) : z * x % (z * y) = z * (x % y)
• Nat.mul_div_mul_left 📋 Init.Data.Nat.Div.Basic
  {m : ℕ} (n k : ℕ) (H : 0 < m) : m * n / (m * k) = n / k
• Nat.mul_div_mul_right 📋 Init.Data.Nat.Div.Basic
  {m : ℕ} (n k : ℕ) (H : 0 < m) : n * m / (k * m) = n / k
• Nat.div_eq_of_lt_le 📋 Init.Data.Nat.Div.Basic
  {k n m : ℕ} (lo : k * n ≤ m) (hi : m < (k + 1) * n) : m / n = k
• Nat.add_mul_div_left 📋 Init.Data.Nat.Div.Basic
  (x z : ℕ) {y : ℕ} (H : 0 < y) : (x + y * z) / y = x / y + z
• Nat.add_mul_div_right 📋 Init.Data.Nat.Div.Basic
  (x y : ℕ) {z : ℕ} (H : 0 < z) : (x + y * z) / z = x / z + y
• Nat.sub_mul_div_of_le 📋 Init.Data.Nat.Div.Basic
  (x n p : ℕ) (h₁ : n * p ≤ x) : (x - n * p) / n = x / n - p
• Nat.mul_sub_div 📋 Init.Data.Nat.Div.Basic
  (x n p : ℕ) (h₁ : x < n * p) : (n * p - (x + 1)) / n = p - (x / n + 1)
• Nat.shiftLeft_eq 📋 Init.Data.Nat.Bitwise.Basic
  (a b : ℕ) : a <<< b = a * 2 ^ b
• Nat.dvd_mul_left 📋 Init.Data.Nat.Dvd
  (a b : ℕ) : a ∣ b * a
• Nat.dvd_mul_right 📋 Init.Data.Nat.Dvd
  (a b : ℕ) : a ∣ a * b
• Nat.dvd_mul_left_of_dvd 📋 Init.Data.Nat.Dvd
  {a b : ℕ} (h : a ∣ b) (c : ℕ) : a ∣ c * b
• Nat.dvd_mul_right_of_dvd 📋 Init.Data.Nat.Dvd
  {a b : ℕ} (h : a ∣ b) (c : ℕ) : a ∣ b * c
• Nat.div_mul_cancel 📋 Init.Data.Nat.Dvd
  {n m : ℕ} (H : n ∣ m) : m / n * n = m
• Nat.mul_div_cancel' 📋 Init.Data.Nat.Dvd
  {n m : ℕ} (H : n ∣ m) : n * (m / n) = m
• Nat.mul_dvd_mul_left 📋 Init.Data.Nat.Dvd
  {b c : ℕ} (a : ℕ) (h : b ∣ c) : a * b ∣ a * c
• Nat.mul_dvd_mul_right 📋 Init.Data.Nat.Dvd
  {a b : ℕ} (h : a ∣ b) (c : ℕ) : a * c ∣ b * c
• Nat.mul_dvd_mul 📋 Init.Data.Nat.Dvd
  {a b c d : ℕ} : a ∣ b → c ∣ d → a * c ∣ b * d
• Nat.dvd_of_mul_dvd_mul_left 📋 Init.Data.Nat.Dvd
  {k m n : ℕ} (kpos : 0 < k) (H : k * m ∣ k * n) : m ∣ n
• Nat.dvd_of_mul_dvd_mul_right 📋 Init.Data.Nat.Dvd
  {k m n : ℕ} (kpos : 0 < k) (H : m * k ∣ n * k) : m ∣ n
• Nat.mul_div_assoc 📋 Init.Data.Nat.Dvd
  {k n : ℕ} (m : ℕ) (H : k ∣ n) : m * n / k = m * (n / k)
• Nat.Linear.Expr.denote_toPoly_go 📋 Init.Data.Nat.Linear
  {k : ℕ} {p : Nat.Linear.Poly} (ctx : Nat.Linear.Context) (e : Nat.Linear.Expr) : Nat.Linear.Poly.denote ctx (Nat.Linear.Expr.toPoly.go k e p) = k * Nat.Linear.Expr.denote ctx e + Nat.Linear.Poly.denote ctx p
• Nat.Linear.Poly.denote_insert 📋 Init.Data.Nat.Linear
  (ctx : Nat.Linear.Context) (k : ℕ) (v : Nat.Linear.Var) (p : Nat.Linear.Poly) : Nat.Linear.Poly.denote ctx (Nat.Linear.Poly.insert k v p) = Nat.Linear.Poly.denote ctx p + k * Nat.Linear.Var.denote ctx v
• Nat.Linear.Poly.denote_cons 📋 Init.Data.Nat.Linear
  (ctx : Nat.Linear.Context) (k : ℕ) (v : Nat.Linear.Var) (p : Nat.Linear.Poly) : Nat.Linear.Poly.denote ctx ((k, v) :: p) = k * Nat.Linear.Var.denote ctx v + Nat.Linear.Poly.denote ctx p
• Nat.mul_max_mul_left 📋 Init.Data.Nat.MinMax
  (a b c : ℕ) : max (a * b) (a * c) = a * max b c
• Nat.mul_max_mul_right 📋 Init.Data.Nat.MinMax
  (a b c : ℕ) : max (a * c) (b * c) = max a b * c
• Nat.mul_min_mul_left 📋 Init.Data.Nat.MinMax
  (a b c : ℕ) : min (a * b) (a * c) = a * min b c
• Nat.mul_min_mul_right 📋 Init.Data.Nat.MinMax
  (a b c : ℕ) : min (a * c) (b * c) = min a b * c
• Int.instAssociativeHMul 📋 Init.Data.Int.Lemmas
  : Std.Associative fun x1 x2 => x1 * x2
• Int.instCommutativeHMul 📋 Init.Data.Int.Lemmas
  : Std.Commutative fun x1 x2 => x1 * x2
• Int.mul_def 📋 Init.Data.Int.Lemmas
  {a b : ℤ} : a.mul b = a * b
• Int.mul_one 📋 Init.Data.Int.Lemmas
  (a : ℤ) : a * 1 = a
• Int.one_mul 📋 Init.Data.Int.Lemmas
  (a : ℤ) : 1 * a = a
• Int.instLawfulIdentityHMulOfNat 📋 Init.Data.Int.Lemmas
  : Std.LawfulIdentity (fun x1 x2 => x1 * x2) 1
• Int.mul_zero 📋 Init.Data.Int.Lemmas
  (a : ℤ) : a * 0 = 0
• Int.zero_mul 📋 Init.Data.Int.Lemmas
  (a : ℤ) : 0 * a = 0
• Int.mul_comm 📋 Init.Data.Int.Lemmas
  (a b : ℤ) : a * b = b * a
• Int.mul_neg_one 📋 Init.Data.Int.Lemmas
  (a : ℤ) : a * -1 = -a
• Int.neg_eq_neg_one_mul 📋 Init.Data.Int.Lemmas
  (a : ℤ) : -a = -1 * a
• Int.neg_one_mul 📋 Init.Data.Int.Lemmas
  (a : ℤ) : -1 * a = -a
• Int.two_mul 📋 Init.Data.Int.Lemmas
  (n : ℤ) : 2 * n = n + n
• Int.negOfNat_mul_negSucc 📋 Init.Data.Int.Lemmas
  (m n : ℕ) : Int.negOfNat n * Int.negSucc m = Int.ofNat (n * m.succ)
• Int.negSucc_mul_negOfNat 📋 Init.Data.Int.Lemmas
  (m n : ℕ) : Int.negSucc m * Int.negOfNat n = Int.ofNat (m.succ * n)
• Int.negOfNat_mul_ofNat 📋 Init.Data.Int.Lemmas
  (m n : ℕ) : Int.negOfNat m * ↑n = Int.negOfNat (m * n)
• Int.ofNat_mul_negOfNat 📋 Init.Data.Int.Lemmas
  (m n : ℕ) : ↑m * Int.negOfNat n = Int.negOfNat (m * n)
• Int.mul_neg 📋 Init.Data.Int.Lemmas
  (a b : ℤ) : a * -b = -(a * b)
• Int.neg_mul 📋 Init.Data.Int.Lemmas
  (a b : ℤ) : -a * b = -(a * b)
• Int.neg_mul_comm 📋 Init.Data.Int.Lemmas
  (a b : ℤ) : -a * b = a * -b
• Int.neg_mul_eq_mul_neg 📋 Init.Data.Int.Lemmas
  (a b : ℤ) : -(a * b) = a * -b
• Int.neg_mul_eq_neg_mul 📋 Init.Data.Int.Lemmas
  (a b : ℤ) : -(a * b) = -a * b
• Int.neg_mul_neg 📋 Init.Data.Int.Lemmas
  (a b : ℤ) : -a * -b = a * b
• Int.eq_one_of_mul_eq_self_left 📋 Init.Data.Int.Lemmas
  {a b : ℤ} (Hpos : a ≠ 0) (H : b * a = a) : b = 1
• Int.eq_one_of_mul_eq_self_right 📋 Init.Data.Int.Lemmas
  {a b : ℤ} (Hpos : b ≠ 0) (H : b * a = b) : a = 1
• Int.instNeZeroHMul 📋 Init.Data.Int.Lemmas
  {a b : ℤ} [NeZero a] [NeZero b] : NeZero (a * b)
• Int.natCast_mul 📋 Init.Data.Int.Lemmas
  (n m : ℕ) : ↑(n * m) = ↑n * ↑m
• Int.ofNat_mul_ofNat 📋 Init.Data.Int.Lemmas
  (m n : ℕ) : ↑m * ↑n = ↑(m * n)
• Int.negSucc_mul_negSucc 📋 Init.Data.Int.Lemmas
  (m n : ℕ) : Int.negSucc m * Int.negSucc n = ↑m.succ * ↑n.succ
• Int.negSucc_mul_ofNat 📋 Init.Data.Int.Lemmas
  (m n : ℕ) : Int.negSucc m * ↑n = -↑(m.succ * n)
• Int.ofNat_mul_negSucc 📋 Init.Data.Int.Lemmas
  (m n : ℕ) : ↑m * Int.negSucc n = -↑(m * n.succ)
• Int.mul_ne_zero 📋 Init.Data.Int.Lemmas
  {a b : ℤ} (a0 : a ≠ 0) (b0 : b ≠ 0) : a * b ≠ 0
• Int.eq_of_mul_eq_mul_left 📋 Init.Data.Int.Lemmas
  {a b c : ℤ} (ha : a ≠ 0) (h : a * b = a * c) : b = c
• Int.eq_of_mul_eq_mul_right 📋 Init.Data.Int.Lemmas
  {a b c : ℤ} (ha : a ≠ 0) (h : b * a = c * a) : b = c
• Int.mul_eq_mul_left_iff 📋 Init.Data.Int.Lemmas
  {a b c : ℤ} (h : c ≠ 0) : c * a = c * b ↔ a = b
• Int.mul_eq_mul_right_iff 📋 Init.Data.Int.Lemmas
  {a b c : ℤ} (h : c ≠ 0) : a * c = b * c ↔ a = b
• Int.mul_eq_zero 📋 Init.Data.Int.Lemmas
  {a b : ℤ} : a * b = 0 ↔ a = 0 ∨ b = 0
• Int.mul_ne_zero_iff 📋 Init.Data.Int.Lemmas
  {a b : ℤ} : a * b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0
• Int.negSucc_mul_subNatNat 📋 Init.Data.Int.Lemmas
  (m n k : ℕ) : Int.negSucc m * Int.subNatNat n k = Int.subNatNat (m.succ * k) (m.succ * n)
• Int.ofNat_mul_subNatNat 📋 Init.Data.Int.Lemmas
  (m n k : ℕ) : ↑m * Int.subNatNat n k = Int.subNatNat (m * n) (m * k)
• Int.mul_assoc 📋 Init.Data.Int.Lemmas
  (a b c : ℤ) : a * b * c = a * (b * c)
• Int.mul_left_comm 📋 Init.Data.Int.Lemmas
  (a b c : ℤ) : a * (b * c) = b * (a * c)
• Int.mul_right_comm 📋 Init.Data.Int.Lemmas
  (a b c : ℤ) : a * b * c = a * c * b
• Int.add_mul 📋 Init.Data.Int.Lemmas
  (a b c : ℤ) : (a + b) * c = a * c + b * c
• Int.mul_add 📋 Init.Data.Int.Lemmas
  (a b c : ℤ) : a * (b + c) = a * b + a * c
• Int.mul_sub 📋 Init.Data.Int.Lemmas
  (a b c : ℤ) : a * (b - c) = a * b - a * c
• Int.sub_mul 📋 Init.Data.Int.Lemmas
  (a b c : ℤ) : (a - b) * c = a * c - b * c
• Int.mul_sign_self 📋 Init.Data.Int.Order
  (i : ℤ) : i * i.sign = ↑i.natAbs
• Int.sign_mul_natAbs 📋 Init.Data.Int.Order
  (a : ℤ) : a.sign * ↑a.natAbs = a
• Int.sign_mul_self 📋 Init.Data.Int.Order
  (i : ℤ) : i.sign * i = ↑i.natAbs
• Int.natAbs_mul 📋 Init.Data.Int.Order
  (a b : ℤ) : (a * b).natAbs = a.natAbs * b.natAbs
• Int.sign_mul 📋 Init.Data.Int.Order
  (a b : ℤ) : (a * b).sign = a.sign * b.sign
• Int.natAbs_mul_self 📋 Init.Data.Int.Order
  {a : ℤ} : ↑(a.natAbs * a.natAbs) = a * a
• Int.natAbs_mul_self' 📋 Init.Data.Int.Order
  (a : ℤ) : ↑a.natAbs * ↑a.natAbs = a * a
• Int.natAbs_mul_natAbs_eq 📋 Init.Data.Int.Order
  {a b : ℤ} {c : ℕ} (h : a * b = ↑c) : a.natAbs * b.natAbs = c
• Int.mul_neg_of_neg_of_pos 📋 Init.Data.Int.Order
  {a b : ℤ} (ha : a < 0) (hb : 0 < b) : a * b < 0
• Int.mul_neg_of_pos_of_neg 📋 Init.Data.Int.Order
  {a b : ℤ} (ha : 0 < a) (hb : b < 0) : a * b < 0
• Int.mul_nonneg 📋 Init.Data.Int.Order
  {a b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a * b
• Int.mul_nonneg_of_nonpos_of_nonpos 📋 Init.Data.Int.Order
  {a b : ℤ} (ha : a ≤ 0) (hb : b ≤ 0) : 0 ≤ a * b
• Int.mul_nonpos_of_nonneg_of_nonpos 📋 Init.Data.Int.Order
  {a b : ℤ} (ha : 0 ≤ a) (hb : b ≤ 0) : a * b ≤ 0
• Int.mul_nonpos_of_nonpos_of_nonneg 📋 Init.Data.Int.Order
  {a b : ℤ} (ha : a ≤ 0) (hb : 0 ≤ b) : a * b ≤ 0
• Int.mul_pos 📋 Init.Data.Int.Order
  {a b : ℤ} (ha : 0 < a) (hb : 0 < b) : 0 < a * b
• Int.mul_pos_of_neg_of_neg 📋 Init.Data.Int.Order
  {a b : ℤ} (ha : a < 0) (hb : b < 0) : 0 < a * b
• Int.mul_self_le_mul_self 📋 Init.Data.Int.Order
  {a b : ℤ} (h1 : 0 ≤ a) (h2 : a ≤ b) : a * a ≤ b * b
• Int.mul_self_lt_mul_self 📋 Init.Data.Int.Order
  {a b : ℤ} (h1 : 0 ≤ a) (h2 : a < b) : a * a < b * b
• Int.neg_of_mul_neg_left 📋 Init.Data.Int.Order
  {a b : ℤ} (h : a * b < 0) (hb : 0 < b) : a < 0
• Int.neg_of_mul_neg_right 📋 Init.Data.Int.Order
  {a b : ℤ} (h : a * b < 0) (ha : 0 < a) : b < 0
• Int.neg_of_mul_pos_left 📋 Init.Data.Int.Order
  {a b : ℤ} (h : 0 < a * b) (hb : b < 0) : a < 0
• Int.neg_of_mul_pos_right 📋 Init.Data.Int.Order
  {a b : ℤ} (h : 0 < a * b) (ha : a < 0) : b < 0
• Int.nonneg_of_mul_nonneg_left 📋 Init.Data.Int.Order
  {a b : ℤ} (h : 0 ≤ a * b) (hb : 0 < b) : 0 ≤ a
• Int.nonneg_of_mul_nonneg_right 📋 Init.Data.Int.Order
  {a b : ℤ} (h : 0 ≤ a * b) (ha : 0 < a) : 0 ≤ b
• Int.nonneg_of_mul_nonpos_left 📋 Init.Data.Int.Order
  {a b : ℤ} (h : a * b ≤ 0) (hb : b < 0) : 0 ≤ a
• Int.nonneg_of_mul_nonpos_right 📋 Init.Data.Int.Order
  {a b : ℤ} (h : a * b ≤ 0) (ha : a < 0) : 0 ≤ b
• Int.nonpos_of_mul_nonneg_left 📋 Init.Data.Int.Order
  {a b : ℤ} (h : 0 ≤ a * b) (hb : b < 0) : a ≤ 0
• Int.nonpos_of_mul_nonneg_right 📋 Init.Data.Int.Order
  {a b : ℤ} (h : 0 ≤ a * b) (ha : a < 0) : b ≤ 0
• Int.nonpos_of_mul_nonpos_left 📋 Init.Data.Int.Order
  {a b : ℤ} (h : a * b ≤ 0) (hb : 0 < b) : a ≤ 0
• Int.nonpos_of_mul_nonpos_right 📋 Init.Data.Int.Order
  {a b : ℤ} (h : a * b ≤ 0) (ha : 0 < a) : b ≤ 0
• Int.pos_of_mul_neg_left 📋 Init.Data.Int.Order
  {a b : ℤ} (h : a * b < 0) (hb : b < 0) : 0 < a
• Int.pos_of_mul_neg_right 📋 Init.Data.Int.Order
  {a b : ℤ} (h : a * b < 0) (ha : a < 0) : 0 < b
• Int.pos_of_mul_pos_left 📋 Init.Data.Int.Order
  {a b : ℤ} (h : 0 < a * b) (hb : 0 < b) : 0 < a
• Int.pos_of_mul_pos_right 📋 Init.Data.Int.Order
  {a b : ℤ} (h : 0 < a * b) (ha : 0 < a) : 0 < b
• Int.mul_le_mul_of_nonneg_left 📋 Init.Data.Int.Order
  {a b c : ℤ} (h₁ : a ≤ b) (h₂ : 0 ≤ c) : c * a ≤ c * b
• Int.mul_le_mul_of_nonneg_right 📋 Init.Data.Int.Order
  {a b c : ℤ} (h₁ : a ≤ b) (h₂ : 0 ≤ c) : a * c ≤ b * c
• Int.mul_le_mul_of_nonpos_left 📋 Init.Data.Int.Order
  {a b c : ℤ} (ha : a ≤ 0) (h : c ≤ b) : a * b ≤ a * c
• Int.mul_le_mul_of_nonpos_right 📋 Init.Data.Int.Order
  {a b c : ℤ} (h : b ≤ a) (hc : c ≤ 0) : a * c ≤ b * c
• Int.mul_lt_mul_of_neg_left 📋 Init.Data.Int.Order
  {a b c : ℤ} (h : b < a) (hc : c < 0) : c * a < c * b
• Int.mul_lt_mul_of_neg_right 📋 Init.Data.Int.Order
  {a b c : ℤ} (h : b < a) (hc : c < 0) : a * c < b * c
• Int.mul_lt_mul_of_pos_left 📋 Init.Data.Int.Order
  {a b c : ℤ} (h₁ : a < b) (h₂ : 0 < c) : c * a < c * b
• Int.mul_lt_mul_of_pos_right 📋 Init.Data.Int.Order
  {a b c : ℤ} (h₁ : a < b) (h₂ : 0 < c) : a * c < b * c
• Int.toNat_mul 📋 Init.Data.Int.Order
  {a b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) : (a * b).toNat = a.toNat * b.toNat
• Int.natAbs_eq_iff_mul_eq_zero 📋 Init.Data.Int.Order
  {a : ℤ} {n : ℕ} : a.natAbs = n ↔ (a - ↑n) * (a + ↑n) = 0
• Int.mul_le_mul 📋 Init.Data.Int.Order
  {a b c d : ℤ} (hac : a ≤ c) (hbd : b ≤ d) (nn_b : 0 ≤ b) (nn_c : 0 ≤ c) : a * b ≤ c * d
• Int.mul_lt_mul 📋 Init.Data.Int.Order
  {a b c d : ℤ} (h₁ : a < c) (h₂ : b ≤ d) (h₃ : 0 < b) (h₄ : 0 ≤ c) : a * b < c * d
• Int.mul_lt_mul' 📋 Init.Data.Int.Order
  {a b c d : ℤ} (h₁ : a ≤ c) (h₂ : b < d) (h₃ : 0 ≤ b) (h₄ : 0 < c) : a * b < c * d
• Lean.Omega.Int.ofNat_mul_nonneg 📋 Init.Omega.Int
  {a b : ℕ} : 0 ≤ ↑a * ↑b
• Lean.Omega.Int.mul_congr_left 📋 Init.Omega.Int
  {a b : ℤ} (h₁ : a = b) (c : ℤ) : a * c = b * c
• Lean.Omega.Int.mul_congr 📋 Init.Omega.Int
  {a b c d : ℤ} (h₁ : a = b) (h₂ : c = d) : a * c = b * d
• Lean.Omega.Int.ofNat_shiftLeft_eq 📋 Init.Omega.Int
  {x y : ℕ} : ↑(x <<< y) = ↑x * ↑(2 ^ y)
• Lean.Omega.Fin.ofNat_val_mul 📋 Init.Omega.Int
  {n : ℕ} {x y : Fin n} : ↑↑(x * y) = ↑↑x * ↑↑y % ↑n
• Int.dvd_mul_left 📋 Init.Data.Int.DivMod.Bootstrap
  (a b : ℤ) : b ∣ a * b
• Int.dvd_mul_right 📋 Init.Data.Int.DivMod.Bootstrap
  (a b : ℤ) : a ∣ a * b
• Int.dvd_def 📋 Init.Data.Int.DivMod.Bootstrap
  (a b : ℤ) : (a ∣ b) = ∃ c, b = a * c
• Int.mul_emod_left 📋 Init.Data.Int.DivMod.Bootstrap
  (a b : ℤ) : a * b % b = 0
• Int.mul_emod_right 📋 Init.Data.Int.DivMod.Bootstrap
  (a b : ℤ) : a * b % a = 0

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.

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 8e80836 serving mathlib revision 7d9358e