Loogle!

Result

Found 1883 declarations mentioning IsOrderedAddMonoid. Of these, only the first 200 are shown.

• IsOrderedAddMonoid 📋 Mathlib.Algebra.Order.Monoid.Defs
  (α : Type u_2) [AddCommMonoid α] [Preorder α] : Prop
• IsOrderedCancelAddMonoid.toIsOrderedAddMonoid 📋 Mathlib.Algebra.Order.Monoid.Defs
  {α : Type u_2} {inst✝ : AddCommMonoid α} {inst✝¹ : Preorder α} [self : IsOrderedCancelAddMonoid α] : IsOrderedAddMonoid α
• IsOrderedAddMonoid.toAddLeftMono 📋 Mathlib.Algebra.Order.Monoid.Defs
  {α : Type u_1} [AddCommMonoid α] [Preorder α] [IsOrderedAddMonoid α] : AddLeftMono α
• IsOrderedAddMonoid.toAddRightMono 📋 Mathlib.Algebra.Order.Monoid.Defs
  {α : Type u_1} [AddCommMonoid α] [Preorder α] [IsOrderedAddMonoid α] : AddRightMono α
• IsOrderedAddMonoid.add_le_add_left 📋 Mathlib.Algebra.Order.Monoid.Defs
  {α : Type u_2} {inst✝ : AddCommMonoid α} {inst✝¹ : Preorder α} [self : IsOrderedAddMonoid α] (a b : α) : a ≤ b → ∀ (c : α), a + c ≤ b + c
• IsOrderedAddMonoid.add_le_add_right 📋 Mathlib.Algebra.Order.Monoid.Defs
  {α : Type u_2} {inst✝ : AddCommMonoid α} {inst✝¹ : Preorder α} [self : IsOrderedAddMonoid α] (a b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b
• add_self_neg_iff 📋 Mathlib.Algebra.Order.Monoid.Defs
  {α : Type u_1} [AddCommMonoid α] [LinearOrder α] [IsOrderedAddMonoid α] {a : α} : a + a < 0 ↔ a < 0
• add_self_nonpos_iff 📋 Mathlib.Algebra.Order.Monoid.Defs
  {α : Type u_1} [AddCommMonoid α] [LinearOrder α] [IsOrderedAddMonoid α] {a : α} : a + a ≤ 0 ↔ a ≤ 0
• nonneg_add_self_iff 📋 Mathlib.Algebra.Order.Monoid.Defs
  {α : Type u_1} [AddCommMonoid α] [LinearOrder α] [IsOrderedAddMonoid α] {a : α} : 0 ≤ a + a ↔ 0 ≤ a
• pos_add_self_iff 📋 Mathlib.Algebra.Order.Monoid.Defs
  {α : Type u_1} [AddCommMonoid α] [LinearOrder α] [IsOrderedAddMonoid α] {a : α} : 0 < a + a ↔ 0 < a
• IsOrderedAddMonoid.mk 📋 Mathlib.Algebra.Order.Monoid.Defs
  {α : Type u_2} [AddCommMonoid α] [Preorder α] (add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a + c ≤ b + c) (add_le_add_right : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b) : IsOrderedAddMonoid α
• IsOrderedCancelAddMonoid.mk 📋 Mathlib.Algebra.Order.Monoid.Defs
  {α : Type u_2} [AddCommMonoid α] [Preorder α] [toIsOrderedAddMonoid : IsOrderedAddMonoid α] (le_of_add_le_add_left : ∀ (a b c : α), a + b ≤ a + c → b ≤ c) (le_of_add_le_add_right : ∀ (a b c : α), b + a ≤ c + a → b ≤ c) : IsOrderedCancelAddMonoid α
• IsOrderedAddMonoid.toIsOrderedCancelAddMonoid 📋 Mathlib.Algebra.Order.Group.Defs
  {α : Type u} [AddCommGroup α] [Preorder α] [IsOrderedAddMonoid α] : IsOrderedCancelAddMonoid α
• IsOrderedAddMonoid.toIsOrderedCancelAddMonoid' 📋 Mathlib.Algebra.Order.Group.Defs
  {α : Type u} [AddCancelCommMonoid α] [LinearOrder α] [IsOrderedAddMonoid α] : IsOrderedCancelAddMonoid α
• LinearOrderedAddCommGroup.to_noMaxOrder 📋 Mathlib.Algebra.Order.Group.Defs
  {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Nontrivial α] : NoMaxOrder α
• LinearOrderedAddCommGroup.to_noMinOrder 📋 Mathlib.Algebra.Order.Group.Defs
  {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Nontrivial α] : NoMinOrder α
• eq_zero_of_neg_eq 📋 Mathlib.Algebra.Order.Group.Defs
  {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a : α} (h : -a = a) : a = 0
• exists_zero_lt 📋 Mathlib.Algebra.Order.Group.Defs
  {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Nontrivial α] : ∃ a, 0 < a
• neg_le_neg 📋 Mathlib.Algebra.Order.Group.Defs
  {α : Type u} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b : α} : a ≤ b → -b ≤ -a
• neg_lt_neg 📋 Mathlib.Algebra.Order.Group.Defs
  {α : Type u} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b : α} : a < b → -b < -a
• neg_neg_of_pos 📋 Mathlib.Algebra.Order.Group.Defs
  {α : Type u} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a : α} : 0 < a → -a < 0
• neg_nonneg_of_nonpos 📋 Mathlib.Algebra.Order.Group.Defs
  {α : Type u} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a : α} : a ≤ 0 → 0 ≤ -a
• neg_nonpos_of_nonneg 📋 Mathlib.Algebra.Order.Group.Defs
  {α : Type u} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a : α} : 0 ≤ a → -a ≤ 0
• le_neg_self_iff 📋 Mathlib.Algebra.Order.Group.Defs
  {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a : α} : a ≤ -a ↔ a ≤ 0
• lt_neg_self_iff 📋 Mathlib.Algebra.Order.Group.Defs
  {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a : α} : a < -a ↔ a < 0
• neg_le_self_iff 📋 Mathlib.Algebra.Order.Group.Defs
  {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a : α} : -a ≤ a ↔ 0 ≤ a
• neg_lt_self_iff 📋 Mathlib.Algebra.Order.Group.Defs
  {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a : α} : -a < a ↔ 0 < a
• IsOrderedRing.toIsOrderedAddMonoid 📋 Mathlib.Algebra.Order.Ring.Defs
  {R : Type u_1} {inst✝ : Semiring R} {inst✝¹ : PartialOrder R} [self : IsOrderedRing R] : IsOrderedAddMonoid R
• IsOrderedRing.mk 📋 Mathlib.Algebra.Order.Ring.Defs
  {R : Type u_1} [Semiring R] [PartialOrder R] [toIsOrderedAddMonoid : IsOrderedAddMonoid R] [toZeroLEOneClass : ZeroLEOneClass R] [toPosMulMono : PosMulMono R] [toMulPosMono : MulPosMono R] : IsOrderedRing R
• IsOrderedRing.of_mul_nonneg 📋 Mathlib.Algebra.Order.Ring.Defs
  {R : Type u} [Ring R] [PartialOrder R] [IsOrderedAddMonoid R] [ZeroLEOneClass R] (mul_nonneg : ∀ (a b : R), 0 ≤ a → 0 ≤ b → 0 ≤ a * b) : IsOrderedRing R
• IsStrictOrderedRing.of_mul_pos 📋 Mathlib.Algebra.Order.Ring.Defs
  {R : Type u} [Ring R] [PartialOrder R] [IsOrderedAddMonoid R] [ZeroLEOneClass R] [Nontrivial R] (mul_pos : ∀ (a b : R), 0 < a → 0 < b → 0 < a * b) : IsStrictOrderedRing R
• exists_nsmul_lt 📋 Mathlib.Algebra.Order.Archimedean.Defs
  {R : Type u_1} [AddCommGroup R] [LinearOrder R] [IsOrderedAddMonoid R] [Archimedean R] {a : R} (ha : a < 0) (b : R) : ∃ n, n • a < b
• le_of_abs_le 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b : G} (h : |a| ≤ b) : a ≤ b
• abs_eq_self 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a : G} : |a| = a ↔ 0 ≤ a
• eq_of_abs_sub_eq_zero 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b : G} (h : |a - b| = 0) : a = b
• neg_le_of_abs_le 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b : G} (h : |a| ≤ b) : -b ≤ a
• abs_eq_neg_self 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a : G} : |a| = -a ↔ a ≤ 0
• eq_of_abs_sub_nonpos 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b : G} (h : |a - b| ≤ 0) : a = b
• abs_sub_nonpos 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b : G} : |a - b| ≤ 0 ↔ a = b
• abs_sub_pos 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b : G} : 0 < |a - b| ↔ a ≠ b
• abs_nsmul 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (n : ℕ) (a : G) : |n • a| = n • |a|
• abs_eq 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b : G} (hb : 0 ≤ b) : |a| = b ↔ a = b ∨ a = -b
• sub_le_of_abs_sub_le_left 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b c : G} (h : |a - b| ≤ c) : b - c ≤ a
• sub_le_of_abs_sub_le_right 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b c : G} (h : |a - b| ≤ c) : a - c ≤ b
• sub_lt_of_abs_sub_lt_left 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b c : G} (h : |a - b| < c) : b - c < a
• sub_lt_of_abs_sub_lt_right 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b c : G} (h : |a - b| < c) : a - c < b
• abs_sub_abs_le_abs_sub 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (a b : G) : |a| - |b| ≤ |a - b|
• abs_le 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b : G} : |a| ≤ b ↔ -b ≤ a ∧ a ≤ b
• le_abs' 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b : G} : a ≤ |b| ↔ b ≤ -a ∨ a ≤ b
• eq_of_abs_sub_lt_all 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {x y : G} (h : ∀ ε > 0, |x - y| < ε) : x = y
• abs_sub 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (a b : G) : |a - b| ≤ |a| + |b|
• abs_sub_abs_le_abs_add 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (a b : G) : |a| - |b| ≤ |a + b|
• apply_abs_le_add_of_nonneg 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {H : Type u_2} [AddZeroClass H] [LE H] [AddLeftMono H] [AddRightMono H] {f : G → H} (h : ∀ (x : G), 0 ≤ f x) (a : G) : f |a| ≤ f a + f (-a)
• apply_abs_le_mul_of_one_le 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {H : Type u_2} [MulOneClass H] [LE H] [MulLeftMono H] [MulRightMono H] {f : G → H} (h : ∀ (x : G), 1 ≤ f x) (a : G) : f |a| ≤ f a * f (-a)
• abs_abs_sub_abs_le_abs_sub 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (a b : G) : ||a| - |b|| ≤ |a - b|
• abs_add' 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (a b : G) : |a| ≤ |b| + |b + a|
• eq_of_abs_sub_le_all 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [DenselyOrdered G] {x y : G} (h : ∀ ε > 0, |x - y| ≤ ε) : x = y
• abs_le_max_abs_abs 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b c : G} (hab : a ≤ b) (hbc : b ≤ c) : |b| ≤ max |a| |c|
• max_zero_add_max_neg_zero_eq_abs_self 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (a : G) : max a 0 + max (-a) 0 = |a|
• abs_sub_le_iff 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b c : G} : |a - b| ≤ c ↔ a - b ≤ c ∧ b - a ≤ c
• abs_sub_lt_iff 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b c : G} : |a - b| < c ↔ a - b < c ∧ b - a < c
• abs_cases 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (a : G) : |a| = a ∧ 0 ≤ a ∨ |a| = -a ∧ a < 0
• apply_abs_le_add_of_nonneg' 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {H : Type u_2} [AddZeroClass H] [LE H] [AddLeftMono H] [AddRightMono H] {f : G → H} {a : G} (h₁ : 0 ≤ f a) (h₂ : 0 ≤ f (-a)) : f |a| ≤ f a + f (-a)
• apply_abs_le_mul_of_one_le' 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {H : Type u_2} [MulOneClass H] [LE H] [MulLeftMono H] [MulRightMono H] {f : G → H} {a : G} (h₁ : 1 ≤ f a) (h₂ : 1 ≤ f (-a)) : f |a| ≤ f a * f (-a)
• abs_sub_le 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (a b c : G) : |a - c| ≤ |a - b| + |b - c|
• abs_sub_le_max_sub 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b c : G} (hac : a ≤ b) (hcd : b ≤ c) (d : G) : |b - d| ≤ max (c - d) (d - a)
• abs_sub_le_of_le_of_le 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b lb ub : G} (hal : lb ≤ a) (hau : a ≤ ub) (hbl : lb ≤ b) (hbu : b ≤ ub) : |a - b| ≤ ub - lb
• abs_add_three 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (a b c : G) : |a + b + c| ≤ |a| + |b| + |c|
• abs_sub_le_of_nonneg_of_le 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b n : G} (nonneg_a : 0 ≤ a) (a_le_n : a ≤ n) (nonneg_b : 0 ≤ b) (b_le_n : b ≤ n) : |a - b| ≤ n
• abs_sub_lt_of_nonneg_of_lt 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b n : G} (nonneg_a : 0 ≤ a) (a_lt_n : a < n) (nonneg_b : 0 ≤ b) (b_lt_n : b < n) : |a - b| < n
• abs_add_eq_add_abs_iff 📋 Mathlib.Algebra.Order.Group.Abs
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (a b : G) : |a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
• Int.instIsOrderedAddMonoid 📋 Mathlib.Algebra.Order.Group.Int
  : IsOrderedAddMonoid ℤ
• CanonicallyOrderedAdd.toIsOrderedAddMonoid 📋 Mathlib.Algebra.Order.Monoid.Canonical.Defs
  {α : Type u} [AddCommMonoid α] [Preorder α] [CanonicallyOrderedAdd α] : IsOrderedAddMonoid α
• Nat.instIsOrderedAddMonoid 📋 Mathlib.Algebra.Order.Group.Nat
  : IsOrderedAddMonoid ℕ
• WithBot.instIsOrderedAddMonoid 📋 Mathlib.Algebra.Order.Monoid.WithTop
  {α : Type u} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] : IsOrderedAddMonoid (WithBot α)
• WithTop.instIsOrderedAddMonoid 📋 Mathlib.Algebra.Order.Monoid.WithTop
  {α : Type u} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] : IsOrderedAddMonoid (WithTop α)
• LinearOrderedAddCommGroupWithTop.toIsOrderedAddMonoid 📋 Mathlib.Algebra.Order.AddGroupWithTop
  {α : Type u_3} [self : LinearOrderedAddCommGroupWithTop α] : IsOrderedAddMonoid α
• LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid 📋 Mathlib.Algebra.Order.AddGroupWithTop
  {α : Type u_3} [self : LinearOrderedAddCommMonoidWithTop α] : IsOrderedAddMonoid α
• WithTop.linearOrderedAddCommMonoidWithTop 📋 Mathlib.Algebra.Order.AddGroupWithTop
  {α : Type u_2} [AddCancelCommMonoid α] [LinearOrder α] [IsOrderedAddMonoid α] : LinearOrderedAddCommMonoidWithTop (WithTop α)
• WithTop.LinearOrderedAddCommGroup.instLinearOrderedAddCommGroupWithTopOfIsOrderedAddMonoid 📋 Mathlib.Algebra.Order.AddGroupWithTop
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] : LinearOrderedAddCommGroupWithTop (WithTop G)
• LinearOrderedAddCommMonoidWithTop.mk 📋 Mathlib.Algebra.Order.AddGroupWithTop
  {α : Type u_3} [toAddCommMonoid : AddCommMonoid α] [toLinearOrder : LinearOrder α] [toIsOrderedAddMonoid : IsOrderedAddMonoid α] [toOrderTop : OrderTop α] (top_add' : ∀ (x : α), ⊤ + x = ⊤) (isAddLeftRegular_of_ne_top : ∀ ⦃x : α⦄, x ≠ ⊤ → IsAddLeftRegular x) : LinearOrderedAddCommMonoidWithTop α
• LinearOrderedAddCommGroupWithTop.mk 📋 Mathlib.Algebra.Order.AddGroupWithTop
  {α : Type u_3} [toAddCommMonoid : AddCommMonoid α] [toLinearOrder : LinearOrder α] [toIsOrderedAddMonoid : IsOrderedAddMonoid α] [toOrderTop : OrderTop α] [toNeg : Neg α] [toSub : Sub α] [toZSMul : ZSMul α] (sub_eq_add_neg : ∀ (a b : α), a - b = a + -b := by intros; rfl) (zsmul_zero' : ∀ (a : α), 0 • a = 0 := by intros; rfl) (zsmul_succ' : ∀ (n : ℕ) (a : α), ↑n.succ • a = ↑n • a + a := by intros; rfl) (zsmul_neg' : ∀ (n : ℕ) (a : α), Int.negSucc n • a = -(↑n.succ • a) := by intros; rfl) [toNontrivial : Nontrivial α] (top_add' : ∀ (x : α), ⊤ + x = ⊤) (neg_top : -⊤ = ⊤) (add_neg_cancel_of_ne_top : ∀ ⦃x : α⦄, x ≠ ⊤ → x + -x = 0) : LinearOrderedAddCommGroupWithTop α
• AddUnits.isOrderedAddMonoid 📋 Mathlib.Algebra.Order.Group.Units
  {α : Type u_1} [AddCommMonoid α] [Preorder α] [IsOrderedAddMonoid α] : IsOrderedAddMonoid (AddUnits α)
• OrderDual.isOrderedAddMonoid 📋 Mathlib.Algebra.Order.Monoid.OrderDual
  {α : Type u} [AddCommMonoid α] [Preorder α] [IsOrderedAddMonoid α] : IsOrderedAddMonoid αᵒᵈ
• Additive.isOrderedAddMonoid 📋 Mathlib.Algebra.Order.Monoid.TypeTags
  {α : Type u_1} [CommMonoid α] [Preorder α] [IsOrderedMonoid α] : IsOrderedAddMonoid (Additive α)
• Multiplicative.isOrderedMonoid 📋 Mathlib.Algebra.Order.Monoid.TypeTags
  {α : Type u_1} [AddCommMonoid α] [Preorder α] [IsOrderedAddMonoid α] : IsOrderedMonoid (Multiplicative α)
• WithZero.isOrderedAddMonoid 📋 Mathlib.Algebra.Order.GroupWithZero.Canonical
  {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] (zero_le : ∀ (a : α), 0 ≤ a) : IsOrderedAddMonoid (WithZero α)
• abs_zsmul 📋 Mathlib.Algebra.Order.Ring.Abs
  {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] (n : ℤ) (a : α) : |n • a| = |n| • |a|
• Function.Injective.isOrderedAddMonoid 📋 Mathlib.Algebra.Order.Monoid.Basic
  {α : Type u} {β : Type u_1} [AddCommMonoid α] [Preorder α] [IsOrderedAddMonoid α] [AddCommMonoid β] [Preorder β] (f : β → α) (add : ∀ (x y : β), f (x + y) = f x + f y) (le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y) : IsOrderedAddMonoid β
• StrictMono.isOrderedAddMonoid 📋 Mathlib.Algebra.Order.Monoid.Basic
  {α : Type u} {β : Type u_1} [AddCommMonoid α] [Preorder α] [IsOrderedAddMonoid α] [AddCommMonoid β] [LinearOrder β] (f : β → α) (hf : StrictMono f) (add : ∀ (x y : β), f (x + y) = f x + f y) : IsOrderedAddMonoid β
• Nonneg.isOrderedAddMonoid 📋 Mathlib.Algebra.Order.Nonneg.Ring
  {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] : IsOrderedAddMonoid (Nonneg α)
• Rat.instIsOrderedAddMonoid 📋 Mathlib.Algebra.Order.Ring.Rat
  : IsOrderedAddMonoid ℚ
• RingSeminormClass.toNonnegHomClass 📋 Mathlib.Algebra.Order.Hom.Basic
  {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [NonUnitalNonAssocRing α] [Semiring β] [LinearOrder β] [IsOrderedAddMonoid β] [RingSeminormClass F α β] : NonnegHomClass F α β
• AddGroupSeminormClass.toNonnegHomClass 📋 Mathlib.Algebra.Order.Hom.Basic
  {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [AddGroup α] [AddCommMonoid β] [LinearOrder β] [IsOrderedAddMonoid β] [AddGroupSeminormClass F α β] : NonnegHomClass F α β
• GroupSeminormClass.toNonnegHomClass 📋 Mathlib.Algebra.Order.Hom.Basic
  {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Group α] [AddCommMonoid β] [LinearOrder β] [IsOrderedAddMonoid β] [GroupSeminormClass F α β] : NonnegHomClass F α β
• map_pos_of_ne_one 📋 Mathlib.Algebra.Order.Hom.Basic
  {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Group α] [AddCommMonoid β] [LinearOrder β] [IsOrderedAddMonoid β] [GroupNormClass F α β] (f : F) {x : α} (hx : x ≠ 1) : 0 < f x
• map_pos_of_ne_zero 📋 Mathlib.Algebra.Order.Hom.Basic
  {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [AddGroup α] [AddCommMonoid β] [LinearOrder β] [IsOrderedAddMonoid β] [AddGroupNormClass F α β] (f : F) {x : α} (hx : x ≠ 0) : 0 < f x
• abs_sub_map_le_div 📋 Mathlib.Algebra.Order.Hom.Basic
  {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Group α] [AddCommGroup β] [LinearOrder β] [IsOrderedAddMonoid β] [GroupSeminormClass F α β] (f : F) (x y : α) : |f x - f y| ≤ f (x / y)
• abs_sub_map_le_sub 📋 Mathlib.Algebra.Order.Hom.Basic
  {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [AddGroup α] [AddCommGroup β] [LinearOrder β] [IsOrderedAddMonoid β] [AddGroupSeminormClass F α β] (f : F) (x y : α) : |f x - f y| ≤ f (x - y)
• not_isAddCyclic_of_denselyOrdered 📋 Mathlib.Algebra.Order.Group.Basic
  (α : Type u_1) [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [DenselyOrdered α] [Nontrivial α] : ¬IsAddCyclic α
• zsmul_mono_right 📋 Mathlib.Algebra.Order.Group.Basic
  (α : Type u_1) [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {n : ℤ} (hn : 0 ≤ n) : Monotone fun x => n • x
• zsmul_strictMono_right 📋 Mathlib.Algebra.Order.Group.Basic
  (α : Type u_1) [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {n : ℤ} (hn : 0 < n) : StrictMono fun x => n • x
• zsmul_left_mono 📋 Mathlib.Algebra.Order.Group.Basic
  {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a : α} (ha : 0 ≤ a) : Monotone fun n => n • a
• zsmul_left_strictAnti 📋 Mathlib.Algebra.Order.Group.Basic
  {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a : α} (ha : a < 0) : StrictAnti fun n => n • a
• zsmul_left_strictMono 📋 Mathlib.Algebra.Order.Group.Basic
  {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a : α} (ha : 0 < a) : StrictMono fun n => n • a
• zsmul_le_zsmul_right 📋 Mathlib.Algebra.Order.Group.Basic
  {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {n : ℤ} {a b : α} (hn : 0 ≤ n) (h : a ≤ b) : n • a ≤ n • b
• zsmul_lt_zsmul_right 📋 Mathlib.Algebra.Order.Group.Basic
  {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {n : ℤ} {a b : α} (hn : 0 < n) (h : a < b) : n • a < n • b
• zsmul_left_inj 📋 Mathlib.Algebra.Order.Group.Basic
  {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a : α} (ha : 0 < a) {m n : ℤ} : m • a = n • a ↔ m = n
• zsmul_le_zsmul_left 📋 Mathlib.Algebra.Order.Group.Basic
  {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {m n : ℤ} {a : α} (ha : 0 ≤ a) (h : m ≤ n) : m • a ≤ n • a
• zsmul_lt_zsmul_left 📋 Mathlib.Algebra.Order.Group.Basic
  {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {m n : ℤ} {a : α} (ha : 0 < a) (h : m < n) : m • a < n • a
• zsmul_le_zsmul_iff_left 📋 Mathlib.Algebra.Order.Group.Basic
  {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {m n : ℤ} {a : α} (ha : 0 < a) : m • a ≤ n • a ↔ m ≤ n
• zsmul_lt_zsmul_iff_left 📋 Mathlib.Algebra.Order.Group.Basic
  {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {m n : ℤ} {a : α} (ha : 0 < a) : m • a < n • a ↔ m < n
• zsmul_le_zsmul_iff_right 📋 Mathlib.Algebra.Order.Group.Basic
  {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {n : ℤ} {a b : α} (hn : 0 < n) : n • a ≤ n • b ↔ a ≤ b
• zsmul_lt_zsmul_iff_right 📋 Mathlib.Algebra.Order.Group.Basic
  {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {n : ℤ} {a b : α} (hn : 0 < n) : n • a < n • b ↔ a < b
• OrderDual.instAddArchimedean 📋 Mathlib.Algebra.Order.Archimedean.Basic
  {G : Type u_1} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] [Archimedean G] : Archimedean Gᵒᵈ
• Nonneg.instArchimedean 📋 Mathlib.Algebra.Order.Archimedean.Basic
  {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] [Archimedean M] : Archimedean (Nonneg M)
• existsUnique_sub_zsmul_mem_Ico 📋 Mathlib.Algebra.Order.Archimedean.Basic
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {a : G} (ha : 0 < a) (b c : G) : ∃! m, b - m • a ∈ Set.Ico c (c + a)
• existsUnique_sub_zsmul_mem_Ioc 📋 Mathlib.Algebra.Order.Archimedean.Basic
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {a : G} (ha : 0 < a) (b c : G) : ∃! m, b - m • a ∈ Set.Ioc c (c + a)
• existsUnique_add_zsmul_mem_Ico 📋 Mathlib.Algebra.Order.Archimedean.Basic
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {a : G} (ha : 0 < a) (b c : G) : ∃! m, b + m • a ∈ Set.Ico c (c + a)
• existsUnique_add_zsmul_mem_Ioc 📋 Mathlib.Algebra.Order.Archimedean.Basic
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {a : G} (ha : 0 < a) (b c : G) : ∃! m, b + m • a ∈ Set.Ioc c (c + a)
• existsUnique_zsmul_near_of_pos 📋 Mathlib.Algebra.Order.Archimedean.Basic
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {a : G} (ha : 0 < a) (g : G) : ∃! k, k • a ≤ g ∧ g < (k + 1) • a
• existsUnique_zsmul_near_of_pos' 📋 Mathlib.Algebra.Order.Archimedean.Basic
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {a : G} (ha : 0 < a) (g : G) : ∃! k, 0 ≤ g - k • a ∧ g - k • a < a
• AddConstMapClass.antitone_iff_Icc 📋 Mathlib.Algebra.AddConstMap.Basic
  {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] [AddConstMapClass F G H a b] {f : F} (ha : 0 < a) (l : G) : Antitone ⇑f ↔ AntitoneOn (⇑f) (Set.Icc l (l + a))
• AddConstMapClass.monotone_iff_Icc 📋 Mathlib.Algebra.AddConstMap.Basic
  {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] [AddConstMapClass F G H a b] {f : F} (ha : 0 < a) (l : G) : Monotone ⇑f ↔ MonotoneOn (⇑f) (Set.Icc l (l + a))
• AddConstMapClass.strictAnti_iff_Icc 📋 Mathlib.Algebra.AddConstMap.Basic
  {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] [AddConstMapClass F G H a b] {f : F} (ha : 0 < a) (l : G) : StrictAnti ⇑f ↔ StrictAntiOn (⇑f) (Set.Icc l (l + a))
• AddConstMapClass.strictMono_iff_Icc 📋 Mathlib.Algebra.AddConstMap.Basic
  {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] [AddConstMapClass F G H a b] {f : F} (ha : 0 < a) (l : G) : StrictMono ⇑f ↔ StrictMonoOn (⇑f) (Set.Icc l (l + a))
• AddConstMapClass.rel_map_of_Icc 📋 Mathlib.Algebra.AddConstMap.Basic
  {F : Type u_1} {G : Type u_2} {H : Type u_3} [FunLike F G H] {a : G} {b : H} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] [AddGroup H] [AddConstMapClass F G H a b] {f : F} {R : H → H → Prop} [IsTrans H R] [hR : CovariantClass H H (fun x y => y + x) R] (ha : 0 < a) {l : G} (hf : ∀ x ∈ Set.Icc l (l + a), ∀ y ∈ Set.Icc l (l + a), x < y → R (f x) (f y)) : Relator.LiftFun (fun x1 x2 => x1 < x2) R ⇑f ⇑f
• List.single_le_sum 📋 Mathlib.Algebra.Order.BigOperators.Group.List
  {M : Type u_3} [AddCommMonoid M] [Preorder M] [IsOrderedAddMonoid M] {l : List M} (hl₁ : ∀ x ∈ l, 0 ≤ x) (x : M) : x ∈ l → x ≤ l.sum
• List.sum_pos 📋 Mathlib.Algebra.Order.BigOperators.Group.List
  {M : Type u_3} [AddCommMonoid M] [Preorder M] [IsOrderedAddMonoid M] (l : List M) : (∀ x ∈ l, 0 < x) → l ≠ [] → 0 < l.sum
• List.sum_eq_zero_iff 📋 Mathlib.Algebra.Order.BigOperators.Group.List
  {M : Type u_3} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] [CanonicallyOrderedAdd M] {l : List M} : l.sum = 0 ↔ ∀ x ∈ l, x = 0
• List.all_zero_of_le_zero_le_of_sum_eq_zero 📋 Mathlib.Algebra.Order.BigOperators.Group.List
  {M : Type u_3} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {l : List M} (hl₁ : ∀ x ∈ l, 0 ≤ x) (hl₂ : l.sum = 0) {x : M} (hx : x ∈ l) : x = 0
• List.le_sum_nonempty_of_subadditive 📋 Mathlib.Algebra.Order.BigOperators.Group.List
  {α : Type u_5} {β : Type u_6} [AddMonoid α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] (f : α → β) (h_add : ∀ (a b : α), f (a + b) ≤ f a + f b) (l : List α) (hs_nonempty : l ≠ ∅) : f l.sum ≤ (List.map f l).sum
• List.le_sum_of_subadditive 📋 Mathlib.Algebra.Order.BigOperators.Group.List
  {α : Type u_5} {β : Type u_6} [AddMonoid α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] (f : α → β) (h_zero : f 0 ≤ 0) (h_add : ∀ (a b : α), f (a + b) ≤ f a + f b) (l : List α) : f l.sum ≤ (List.map f l).sum
• List.le_sum_nonempty_of_subadditive_on_pred 📋 Mathlib.Algebra.Order.BigOperators.Group.List
  {α : Type u_5} {β : Type u_6} [AddMonoid α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] (f : α → β) (p : α → Prop) (h_add : ∀ (a b : α), p a → p b → f (a + b) ≤ f a + f b) (hp_add : ∀ (a b : α), p a → p b → p (a + b)) (l : List α) (hl_nonempty : l ≠ []) (hl : ∀ a ∈ l, p a) : f l.sum ≤ (List.map f l).sum
• List.le_sum_of_subadditive_on_pred 📋 Mathlib.Algebra.Order.BigOperators.Group.List
  {α : Type u_5} {β : Type u_6} [AddMonoid α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] (f : α → β) (p : α → Prop) (h_zero : f 0 ≤ 0) (hp_zero : p 0) (h_add : ∀ (a b : α), p a → p b → f (a + b) ≤ f a + f b) (hp_add : ∀ (a b : α), p a → p b → p (a + b)) (l : List α) (hpl : ∀ a ∈ l, p a) : f l.sum ≤ (List.map f l).sum
• OrderAddMonoidHom.instAddOfIsOrderedAddMonoid 📋 Mathlib.Algebra.Order.Hom.Monoid
  {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [Preorder α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] : Add (α →+o β)
• antitone_iff_map_nonneg 📋 Mathlib.Algebra.Order.Hom.Monoid
  {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [i : FunLike F α β] (f : F) [iamhc : AddMonoidHomClass F α β] : Antitone ⇑f ↔ ∀ a ≤ 0, 0 ≤ f a
• antitone_iff_map_nonpos 📋 Mathlib.Algebra.Order.Hom.Monoid
  {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [i : FunLike F α β] (f : F) [iamhc : AddMonoidHomClass F α β] : Antitone ⇑f ↔ ∀ (a : α), 0 ≤ a → f a ≤ 0
• monotone_iff_map_nonneg 📋 Mathlib.Algebra.Order.Hom.Monoid
  {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [i : FunLike F α β] (f : F) [iamhc : AddMonoidHomClass F α β] : Monotone ⇑f ↔ ∀ (a : α), 0 ≤ a → 0 ≤ f a
• monotone_iff_map_nonpos 📋 Mathlib.Algebra.Order.Hom.Monoid
  {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [i : FunLike F α β] (f : F) [iamhc : AddMonoidHomClass F α β] : Monotone ⇑f ↔ ∀ a ≤ 0, f a ≤ 0
• strictAnti_iff_map_neg 📋 Mathlib.Algebra.Order.Hom.Monoid
  {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [i : FunLike F α β] (f : F) [iamhc : AddMonoidHomClass F α β] : StrictAnti ⇑f ↔ ∀ (a : α), 0 < a → f a < 0
• strictAnti_iff_map_pos 📋 Mathlib.Algebra.Order.Hom.Monoid
  {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [i : FunLike F α β] (f : F) [iamhc : AddMonoidHomClass F α β] : StrictAnti ⇑f ↔ ∀ a < 0, 0 < f a
• strictMono_iff_map_neg 📋 Mathlib.Algebra.Order.Hom.Monoid
  {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [i : FunLike F α β] (f : F) [iamhc : AddMonoidHomClass F α β] : StrictMono ⇑f ↔ ∀ a < 0, f a < 0
• strictMono_iff_map_pos 📋 Mathlib.Algebra.Order.Hom.Monoid
  {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [i : FunLike F α β] (f : F) [iamhc : AddMonoidHomClass F α β] : StrictMono ⇑f ↔ ∀ (a : α), 0 < a → 0 < f a
• OrderAddMonoidHom.add_apply 📋 Mathlib.Algebra.Order.Hom.Monoid
  {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [Preorder α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] (f g : α →+o β) (a : α) : (f + g) a = f a + g a
• OrderAddMonoidHom.coe_add 📋 Mathlib.Algebra.Order.Hom.Monoid
  {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [Preorder α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] (f g : α →+o β) : ⇑(f + g) = ⇑f + ⇑g
• OrderAddMonoidHom.add_comp 📋 Mathlib.Algebra.Order.Hom.Monoid
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddCommMonoid α] [Preorder α] [AddCommMonoid β] [Preorder β] [AddCommMonoid γ] [Preorder γ] [IsOrderedAddMonoid γ] (g₁ g₂ : β →+o γ) (f : α →+o β) : (g₁ + g₂).comp f = g₁.comp f + g₂.comp f
• OrderAddMonoidHom.comp_add 📋 Mathlib.Algebra.Order.Hom.Monoid
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddCommMonoid α] [Preorder α] [AddCommMonoid β] [Preorder β] [AddCommMonoid γ] [Preorder γ] [IsOrderedAddMonoid β] [IsOrderedAddMonoid γ] (g : β →+o γ) (f₁ f₂ : α →+o β) : g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂
• Submodule.instIsOrderedAddMonoid 📋 Mathlib.Algebra.Module.Submodule.Pointwise
  {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : IsOrderedAddMonoid (Submodule R M)
• Multiset.single_le_sum 📋 Mathlib.Algebra.Order.BigOperators.Group.Multiset
  {α : Type u_2} [AddCommMonoid α] [Preorder α] {s : Multiset α} [IsOrderedAddMonoid α] : (∀ x ∈ s, 0 ≤ x) → ∀ x ∈ s, x ≤ s.sum
• Multiset.abs_sum_le_sum_abs 📋 Mathlib.Algebra.Order.BigOperators.Group.Multiset
  {α : Type u_2} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {s : Multiset α} : |s.sum| ≤ (Multiset.map abs s).sum
• Multiset.sum_eq_zero_iff 📋 Mathlib.Algebra.Order.BigOperators.Group.Multiset
  {α : Type u_2} [AddCommMonoid α] {m : Multiset α} [PartialOrder α] [CanonicallyOrderedAdd α] [IsOrderedAddMonoid α] : m.sum = 0 ↔ ∀ x ∈ m, x = 0
• Multiset.le_sum_nonempty_of_subadditive 📋 Mathlib.Algebra.Order.BigOperators.Group.Multiset
  {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] (f : α → β) (h_add : ∀ (a b : α), f (a + b) ≤ f a + f b) (s : Multiset α) (hs_nonempty : s ≠ ∅) : f s.sum ≤ (Multiset.map f s).sum
• Multiset.all_zero_of_le_zero_le_of_sum_eq_zero 📋 Mathlib.Algebra.Order.BigOperators.Group.Multiset
  {α : Type u_4} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] {s : Multiset α} : (∀ x ∈ s, 0 ≤ x) → s.sum = 0 → ∀ x ∈ s, x = 0
• Multiset.max_sum_le 📋 Mathlib.Algebra.Order.BigOperators.Group.Multiset
  {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] [LinearOrder α] [IsOrderedAddMonoid α] {s : Multiset ι} {f g : ι → α} : max (Multiset.map f s).sum (Multiset.map g s).sum ≤ (Multiset.map (fun i => max (f i) (g i)) s).sum
• Multiset.sum_min_le 📋 Mathlib.Algebra.Order.BigOperators.Group.Multiset
  {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] [LinearOrder α] [IsOrderedAddMonoid α] {s : Multiset ι} {f g : ι → α} : (Multiset.map (fun i => min (f i) (g i)) s).sum ≤ min (Multiset.map f s).sum (Multiset.map g s).sum
• Multiset.le_sum_of_subadditive 📋 Mathlib.Algebra.Order.BigOperators.Group.Multiset
  {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] (f : α → β) (h_zero : f 0 ≤ 0) (h_add : ∀ (a b : α), f (a + b) ≤ f a + f b) (s : Multiset α) : f s.sum ≤ (Multiset.map f s).sum
• Multiset.le_sum_nonempty_of_subadditive_on_pred 📋 Mathlib.Algebra.Order.BigOperators.Group.Multiset
  {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] (f : α → β) (p : α → Prop) (h_add : ∀ (a b : α), p a → p b → f (a + b) ≤ f a + f b) (hp_add : ∀ (a b : α), p a → p b → p (a + b)) (s : Multiset α) (hs_nonempty : s ≠ ∅) (hs : ∀ a ∈ s, p a) : f s.sum ≤ (Multiset.map f s).sum
• Multiset.le_sum_of_subadditive_on_pred 📋 Mathlib.Algebra.Order.BigOperators.Group.Multiset
  {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] (f : α → β) (p : α → Prop) (h_zero : f 0 ≤ 0) (hp_zero : p 0) (h_add : ∀ (a b : α), p a → p b → f (a + b) ≤ f a + f b) (hp_add : ∀ (a b : α), p a → p b → p (a + b)) (s : Multiset α) (hps : ∀ a ∈ s, p a) : f s.sum ≤ (Multiset.map f s).sum
• Finset.abs_sum_le_sum_abs 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
  {ι : Type u_1} {G : Type u_8} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (f : ι → G) (s : Finset ι) : |∑ i ∈ s, f i| ≤ ∑ i ∈ s, |f i|
• Finset.max_sum_le 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
  {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [LinearOrder M] [IsOrderedAddMonoid M] {f g : ι → M} {s : Finset ι} : max (s.sum f) (s.sum g) ≤ ∑ i ∈ s, max (f i) (g i)
• Finset.sum_min_le 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
  {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [LinearOrder M] [IsOrderedAddMonoid M] {f g : ι → M} {s : Finset ι} : ∑ i ∈ s, min (f i) (g i) ≤ min (s.sum f) (s.sum g)
• Finset.le_sum_nonempty_of_subadditive 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
  {ι : Type u_1} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Preorder N] [IsOrderedAddMonoid N] (f : M → N) (h_add : ∀ (x y : M), f (x + y) ≤ f x + f y) {s : Finset ι} (hs : s.Nonempty) (g : ι → M) : f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i)
• Finset.le_sum_of_subadditive 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
  {ι : Type u_1} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Preorder N] [IsOrderedAddMonoid N] (f : M → N) (h_zero : f 0 ≤ 0) (h_add : ∀ (x y : M), f (x + y) ≤ f x + f y) (s : Finset ι) (g : ι → M) : f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i)
• Finset.le_sum_nonempty_of_subadditive_on_pred 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
  {ι : Type u_1} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Preorder N] [IsOrderedAddMonoid N] (f : M → N) (p : M → Prop) (h_add : ∀ (x y : M), p x → p y → f (x + y) ≤ f x + f y) (hp_add : ∀ (x y : M), p x → p y → p (x + y)) (g : ι → M) (s : Finset ι) (hs_nonempty : s.Nonempty) (hs : ∀ i ∈ s, p (g i)) : f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i)
• Finset.le_sum_of_subadditive_on_pred 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
  {ι : Type u_1} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Preorder N] [IsOrderedAddMonoid N] (f : M → N) (p : M → Prop) (h_zero : f 0 ≤ 0) (h_add : ∀ (x y : M), p x → p y → f (x + y) ≤ f x + f y) (hp_add : ∀ (x y : M), p x → p y → p (x + y)) (g : ι → M) {s : Finset ι} (hs : ∀ i ∈ s, p (g i)) : f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i)
• finsum_nonneg 📋 Mathlib.Algebra.BigOperators.Finprod
  {α : Sort u_4} {M : Type u_6} [AddCommMonoid M] [Preorder M] [IsOrderedAddMonoid M] {f : α → M} (hf : ∀ (i : α), 0 ≤ f i) : 0 ≤ ∑ᶠ (i : α), f i
• single_le_finsum 📋 Mathlib.Algebra.BigOperators.Finprod
  {α : Type u_1} {M : Type u_7} [AddCommMonoid M] [Preorder M] [IsOrderedAddMonoid M] (i : α) {f : α → M} (hf : Function.HasFiniteSupport f) (h : ∀ (j : α), 0 ≤ f j) : f i ≤ ∑ᶠ (j : α), f j
• instPosSMulMonoNatOfIsOrderedAddMonoid 📋 Mathlib.Algebra.Order.Module.Defs
  {M : Type u_3} [PartialOrder M] [AddCommMonoid M] [IsOrderedAddMonoid M] : PosSMulMono ℕ M
• instPosSMulStrictMonoNatOfIsOrderedAddMonoid 📋 Mathlib.Algebra.Order.Module.Defs
  {M : Type u_3} [PartialOrder M] [AddCancelCommMonoid M] [IsOrderedAddMonoid M] : PosSMulStrictMono ℕ M
• instPosSMulStrictMonoIntOfIsOrderedAddMonoid 📋 Mathlib.Algebra.Order.Module.Defs
  {G : Type u_3} [PartialOrder G] [AddCommGroup G] [IsOrderedAddMonoid G] : PosSMulStrictMono ℤ G
• instSMulPosMonoNatOfIsOrderedAddMonoid 📋 Mathlib.Algebra.Order.Module.Defs
  {M : Type u_3} [PartialOrder M] [AddCommMonoid M] [IsOrderedAddMonoid M] : SMulPosMono ℕ M
• instSMulPosStrictMonoIntOfIsOrderedAddMonoid 📋 Mathlib.Algebra.Order.Module.Defs
  {G : Type u_3} [PartialOrder G] [AddCommGroup G] [IsOrderedAddMonoid G] : SMulPosStrictMono ℤ G
• OrderDual.instSMulPosMono 📋 Mathlib.Algebra.Order.Module.Defs
  {α : Type u_1} {β : Type u_2} [Preorder α] [Monoid α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [DistribMulAction α β] [SMulPosMono α β] : SMulPosMono α βᵒᵈ
• OrderDual.instSMulPosReflectLE 📋 Mathlib.Algebra.Order.Module.Defs
  {α : Type u_1} {β : Type u_2} [Preorder α] [Monoid α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [DistribMulAction α β] [SMulPosReflectLE α β] : SMulPosReflectLE α βᵒᵈ
• OrderDual.instSMulPosReflectLT 📋 Mathlib.Algebra.Order.Module.Defs
  {α : Type u_1} {β : Type u_2} [Preorder α] [Monoid α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [DistribMulAction α β] [SMulPosReflectLT α β] : SMulPosReflectLT α βᵒᵈ
• OrderDual.instSMulPosStrictMono 📋 Mathlib.Algebra.Order.Module.Defs
  {α : Type u_1} {β : Type u_2} [Preorder α] [Monoid α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [DistribMulAction α β] [SMulPosStrictMono α β] : SMulPosStrictMono α βᵒᵈ
• OrderDual.instIsOrderedModule 📋 Mathlib.Algebra.Order.Module.Defs
  {α : Type u_1} {β : Type u_2} [Preorder α] [MonoidWithZero α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [DistribMulAction α β] [IsOrderedModule α β] : IsOrderedModule α βᵒᵈ
• OrderDual.instIsStrictOrderedModule 📋 Mathlib.Algebra.Order.Module.Defs
  {α : Type u_1} {β : Type u_2} [Preorder α] [MonoidWithZero α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [DistribMulAction α β] [IsStrictOrderedModule α β] : IsStrictOrderedModule α βᵒᵈ
• PosSMulMono.toSMulPosMono 📋 Mathlib.Algebra.Order.Module.Defs
  {α : Type u_1} {β : Type u_2} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulMono α β] : SMulPosMono α β
• PosSMulStrictMono.toSMulPosStrictMono 📋 Mathlib.Algebra.Order.Module.Defs
  {α : Type u_1} {β : Type u_2} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulStrictMono α β] : SMulPosStrictMono α β
• antitone_smul_left 📋 Mathlib.Algebra.Order.Module.Defs
  {α : Type u_1} {β : Type u_2} {a : α} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulMono α β] (ha : a ≤ 0) : Antitone fun x => a • x
• strictAnti_smul_left 📋 Mathlib.Algebra.Order.Module.Defs
  {α : Type u_1} {β : Type u_2} {a : α} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulStrictMono α β] (ha : a < 0) : StrictAnti fun x => a • x
• PosSMulMono.of_smul_nonneg 📋 Mathlib.Algebra.Order.Module.Defs
  {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommGroup β] [Module α β] [PartialOrder α] [PartialOrder β] [IsOrderedAddMonoid β] (h : ∀ (a : α), 0 ≤ a → ∀ (b : β), 0 ≤ b → 0 ≤ a • b) : PosSMulMono α β
• smul_nonneg_of_nonpos_of_nonpos 📋 Mathlib.Algebra.Order.Module.Defs
  {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Ring α] [PartialOrder α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [SMulPosMono α β] (ha : a ≤ 0) (hb : b ≤ 0) : 0 ≤ a • b
• IsOrderedModule.of_smul_nonneg 📋 Mathlib.Algebra.Order.Module.Defs
  {α : Type u_1} {β : Type u_2} [Ring α] [AddCommGroup β] [Module α β] [PartialOrder α] [PartialOrder β] [IsOrderedAddMonoid α] [IsOrderedAddMonoid β] (h : ∀ (a : α), 0 ≤ a → ∀ (b : β), 0 ≤ b → 0 ≤ a • b) : IsOrderedModule α β
• le_of_smul_le_smul_of_neg 📋 Mathlib.Algebra.Order.Module.Defs
  {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulReflectLE α β] (h : a • b₁ ≤ a • b₂) (ha : a < 0) : b₂ ≤ b₁
• lt_of_smul_lt_smul_of_nonpos 📋 Mathlib.Algebra.Order.Module.Defs
  {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulReflectLT α β] (h : a • b₁ < a • b₂) (ha : a ≤ 0) : b₂ < b₁
• smul_le_smul_of_nonpos_left 📋 Mathlib.Algebra.Order.Module.Defs
  {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulMono α β] (h : b₁ ≤ b₂) (ha : a ≤ 0) : a • b₂ ≤ a • b₁
• smul_lt_smul_of_neg_left 📋 Mathlib.Algebra.Order.Module.Defs
  {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulStrictMono α β] (hb : b₁ < b₂) (ha : a < 0) : a • b₂ < a • b₁
• smul_pos_of_neg_of_neg 📋 Mathlib.Algebra.Order.Module.Defs
  {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : a < 0) : b < 0 → 0 < a • b
• smul_neg_iff_of_neg_left 📋 Mathlib.Algebra.Order.Module.Defs
  {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : a < 0) : a • b < 0 ↔ 0 < b
• smul_pos_iff_of_neg_left 📋 Mathlib.Algebra.Order.Module.Defs
  {α : Type u_1} {β : Type u_2} {a : α} {b : β} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : a < 0) : 0 < a • b ↔ b < 0
• smul_le_smul_iff_of_neg_left 📋 Mathlib.Algebra.Order.Module.Defs
  {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulMono α β] [PosSMulReflectLE α β] (ha : a < 0) : a • b₁ ≤ a • b₂ ↔ b₂ ≤ b₁
• smul_lt_smul_iff_of_neg_left 📋 Mathlib.Algebra.Order.Module.Defs
  {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : a < 0) : a • b₁ < a • b₂ ↔ b₂ < b₁
• smul_nonneg_iff_neg_imp_nonpos 📋 Mathlib.Algebra.Order.Module.Defs
  {α : Type u_1} {β : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [AddCommGroup β] [LinearOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulStrictMono α β] {a : α} {b : β} : 0 ≤ a • b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)
• smul_nonneg_iff_pos_imp_nonneg 📋 Mathlib.Algebra.Order.Module.Defs
  {α : Type u_1} {β : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [AddCommGroup β] [LinearOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulStrictMono α β] {a : α} {b : β} : 0 ≤ a • b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)
• smul_nonpos_iff_neg_imp_nonneg 📋 Mathlib.Algebra.Order.Module.Defs
  {α : Type u_1} {β : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [AddCommGroup β] [LinearOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulStrictMono α β] {a : α} {b : β} : a • b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)
• smul_nonpos_iff_pos_imp_nonpos 📋 Mathlib.Algebra.Order.Module.Defs
  {α : Type u_1} {β : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [AddCommGroup β] [LinearOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulStrictMono α β] {a : α} {b : β} : a • b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)
• nonneg_and_nonneg_or_nonpos_and_nonpos_of_smul_nonneg 📋 Mathlib.Algebra.Order.Module.Defs
  {α : Type u_1} {β : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [AddCommGroup β] [LinearOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulStrictMono α β] {a : α} {b : β} (hab : 0 ≤ a • b) : 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

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 69fae59