Loogle!

Result

Found 178 declarations mentioning AddRightStrictMono.

• AddRightStrictMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  (M : Type u_1) [Add M] [LT M] : Prop
• addRightMono_of_addRightStrictMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  (M : Type u_3) [Add M] [PartialOrder M] [AddRightStrictMono M] : AddRightMono M
• addRightStrictMono_of_addLeftStrictMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  (N : Type u_2) [AddCommSemigroup N] [LT N] [AddLeftStrictMono N] : AddRightStrictMono N
• IsRightCancelAdd.addRightStrictMono_of_addRightMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  (N : Type u_2) [Add N] [IsRightCancelAdd N] [PartialOrder N] [AddRightMono N] : AddRightStrictMono N
• addRightStrictMono_of_addRightReflectLE 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  (N : Type u_2) [Add N] [LinearOrder N] [AddRightReflectLE N] : AddRightStrictMono N
• AddGroup.addRightReflectLT_of_addRightStrictMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  {N : Type u_2} [AddGroup N] [LT N] [AddRightStrictMono N] : AddRightReflectLT N
• AddRightStrictMono.toIsRightCancelAdd 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} [Add α] [LinearOrder α] [AddRightStrictMono α] : IsRightCancelAdd α
• add_left_strictMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {a : α} [Add α] [Preorder α] [AddRightStrictMono α] : StrictMono fun x => x + a
• add_lt_add_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {b c : α} [Add α] [LT α] [i : AddRightStrictMono α] (bc : b < c) (a : α) : b + a < c + a
• StrictAnti.add_const 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : β → α} [AddRightStrictMono α] (hf : StrictAnti f) (c : α) : StrictAnti fun x => f x + c
• StrictMono.add_const 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : β → α} [AddRightStrictMono α] (hf : StrictMono f) (c : α) : StrictMono fun x => f x + c
• addRightStrictMono_iff_addRightMono_and_isRightCancelAdd 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} [Add α] [LinearOrder α] : AddRightStrictMono α ↔ AddRightMono α ∧ IsRightCancelAdd α
• add_lt_add_iff_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {b c : α} [Add α] [LT α] [AddRightStrictMono α] [AddRightReflectLT α] (a : α) : b + a < c + a ↔ b < c
• StrictAntiOn.add_const 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : β → α} {s : Set β} [AddRightStrictMono α] (hf : StrictAntiOn f s) (c : α) : StrictAntiOn (fun x => f x + c) s
• StrictMonoOn.add_const 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : β → α} {s : Set β} [AddRightStrictMono α] (hf : StrictMonoOn f s) (c : α) : StrictMonoOn (fun x => f x + c) s
• add_lt_of_neg_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {b : α} [AddZeroClass α] [LT α] [AddRightStrictMono α] (a : α) (h : b < 0) : b + a < a
• lt_add_of_pos_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {b : α} [AddZeroClass α] [LT α] [AddRightStrictMono α] (a : α) (h : 0 < b) : a < b + a
• StrictAnti.add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f g : β → α} [AddLeftStrictMono α] [AddRightStrictMono α] (hf : StrictAnti f) (hg : StrictAnti g) : StrictAnti fun x => f x + g x
• StrictAnti.add_antitone 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f g : β → α} [AddLeftMono α] [AddRightStrictMono α] (hf : StrictAnti f) (hg : Antitone g) : StrictAnti fun x => f x + g x
• StrictMono.add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f g : β → α} [AddLeftStrictMono α] [AddRightStrictMono α] (hf : StrictMono f) (hg : StrictMono g) : StrictMono fun x => f x + g x
• StrictMono.add_monotone 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f g : β → α} [AddLeftMono α] [AddRightStrictMono α] (hf : StrictMono f) (hg : Monotone g) : StrictMono fun x => f x + g x
• add_lt_iff_neg_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {a : α} [AddZeroClass α] [LT α] [AddRightStrictMono α] [AddRightReflectLT α] (b : α) : a + b < b ↔ a < 0
• lt_add_iff_pos_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {b : α} [AddZeroClass α] [LT α] [AddRightStrictMono α] [AddRightReflectLT α] (a : α) : a < b + a ↔ 0 < b
• add_lt_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {a b c d : α} [Add α] [Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α] (h₁ : a < b) (h₂ : c < d) : a + c < b + d
• add_lt_add_of_lt_of_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {a b c d : α} [Add α] [Preorder α] [AddLeftMono α] [AddRightStrictMono α] (h₁ : a < b) (h₂ : c ≤ d) : a + c < b + d
• add_lt_add_of_lt_of_lt 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {a b c d : α} [Add α] [Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α] (h₁ : a < b) (h₂ : c < d) : a + c < b + d
• Right.add_lt_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {a b c d : α} [Add α] [Preorder α] [AddLeftMono α] [AddRightStrictMono α] (h₁ : a < b) (h₂ : c < d) : a + c < b + d
• StrictAntiOn.add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f g : β → α} {s : Set β} [AddLeftStrictMono α] [AddRightStrictMono α] (hf : StrictAntiOn f s) (hg : StrictAntiOn g s) : StrictAntiOn (fun x => f x + g x) s
• StrictAntiOn.add_antitone 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f g : β → α} {s : Set β} [AddLeftMono α] [AddRightStrictMono α] (hf : StrictAntiOn f s) (hg : AntitoneOn g s) : StrictAntiOn (fun x => f x + g x) s
• StrictMonoOn.add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f g : β → α} {s : Set β} [AddLeftStrictMono α] [AddRightStrictMono α] (hf : StrictMonoOn f s) (hg : StrictMonoOn g s) : StrictMonoOn (fun x => f x + g x) s
• StrictMonoOn.add_monotone 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f g : β → α} {s : Set β} [AddLeftMono α] [AddRightStrictMono α] (hf : StrictMonoOn f s) (hg : MonotoneOn g s) : StrictMonoOn (fun x => f x + g x) s
• add_left_inj_of_comparable 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {a b c : α} [Add α] [PartialOrder α] [AddRightStrictMono α] (h : b ≤ c ∨ c ≤ b) : c + a = b + a ↔ c = b
• add_lt_of_neg_of_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddRightStrictMono α] (ha : a < 0) (hbc : b ≤ c) : a + b < c
• add_lt_of_neg_of_lt 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddRightStrictMono α] (ha : a < 0) (hbc : b < c) : a + b < c
• lt_add_of_pos_of_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddRightStrictMono α] (ha : 0 < a) (hbc : b ≤ c) : b < a + c
• lt_add_of_pos_of_lt 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddRightStrictMono α] (ha : 0 < a) (hbc : b < c) : b < a + c
• Right.add_neg 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddRightStrictMono α] (ha : a < 0) (hbc : b < c) : a + b < c
• Right.add_neg_of_neg_of_nonpos 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddRightStrictMono α] (ha : a < 0) (hbc : b ≤ c) : a + b < c
• Right.add_pos 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddRightStrictMono α] (ha : 0 < a) (hbc : b < c) : b < a + c
• Right.add_pos_of_pos_of_nonneg 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {a b c : α} [AddZeroClass α] [Preorder α] [AddRightStrictMono α] (ha : 0 < a) (hbc : b ≤ c) : b < a + c
• Right.pos_add_of_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} [AddZeroClass α] [Preorder α] [IsBotZeroClass α] [AddRightStrictMono α] {a : α} (ha : 0 < a) (b : α) : 0 < a + b
• add_eq_add_iff_eq_and_eq 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {a b c d : α} [Add α] [PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] (hac : a ≤ c) (hbd : b ≤ d) : a + b = c + d ↔ a = c ∧ b = d
• add_le_add_iff_of_ge 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} [Add α] [PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] {a₁ a₂ b₁ b₂ : α} (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) : a₂ + b₂ ≤ a₁ + b₁ ↔ a₁ = a₂ ∧ b₁ = b₂
• cmp_add_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_3} [Add α] [LinearOrder α] [AddRightStrictMono α] (a b c : α) : cmp (a + c) (b + c) = cmp a b
• trichotomy_of_add_eq_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {a b c d : α} [Add α] [LinearOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] (h : a + b = c + d) : a = c ∧ b = d ∨ a < c ∨ b < d
• min_le_max_of_add_le_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {a b c d : α} [Add α] [LinearOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] (h : a + b ≤ c + d) : min a b ≤ max c d
• Right.min_le_max_of_add_le_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
  {α : Type u_1} {a b c d : α} [Add α] [LinearOrder α] [AddLeftMono α] [AddRightStrictMono α] (h : a + b ≤ c + d) : min a b ≤ max c d
• lt_of_sub_neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} : a - b < 0 → a < b
• lt_of_sub_pos 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} : 0 < a - b → b < a
• sub_lt_sub_right 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} (h : a < b) (c : α) : a - c < b - c
• sub_neg_of_lt 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} : a < b → a - b < 0
• sub_pos_of_lt 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} : b < a → 0 < a - b
• sub_lt_sub_iff_right 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} (c : α) : a - c < b - c ↔ a < b
• sub_lt_zero 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} : a - b < 0 ↔ a < b
• sub_neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} : a - b < 0 ↔ a < b
• sub_pos 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} : 0 < a - b ↔ b < a
• Right.neg_lt_self 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [Preorder α] [AddRightStrictMono α] {a : α} (h : 0 < a) : -a < a
• Right.self_lt_neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [Preorder α] [AddRightStrictMono α] {a : α} (h : a < 0) : a < -a
• add_lt_of_lt_sub_right 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b c : α} : a < c - b → a + b < c
• lt_add_of_sub_right_lt 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b c : α} : a - c < b → a < b + c
• lt_sub_right_of_add_lt 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b c : α} : a + b < c → a < c - b
• sub_right_lt_of_lt_add 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b c : α} : a < b + c → a - c < b
• lt_sub_iff_add_lt 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b c : α} : a < c - b ↔ a + b < c
• sub_lt_iff_lt_add 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b c : α} : a - c < b ↔ a < b + c
• lt_neg_of_lt_neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b : α} [AddRightStrictMono α] : a < -b → b < -a
• lt_of_neg_lt_neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b : α} [AddRightStrictMono α] : -a < -b → b < a
• neg_lt_of_neg_lt 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b : α} [AddRightStrictMono α] : -a < b → -b < a
• StrictAnti.neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α] [Preorder β] {f : β → α} (hf : StrictAnti f) : StrictMono fun x => -f x
• StrictMono.neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α] [Preorder β] {f : β → α} (hf : StrictMono f) : StrictAnti fun x => -f x
• lt_neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b : α} [AddRightStrictMono α] : a < -b ↔ b < -a
• neg_lt 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b : α} [AddRightStrictMono α] : -a < b ↔ -b < a
• neg_lt_neg_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b : α} [AddRightStrictMono α] : -a < -b ↔ b < a
• Right.neg_neg_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a : α} : -a < 0 ↔ 0 < a
• Right.neg_pos_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a : α} : 0 < -a ↔ a < 0
• sub_lt_sub_left 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] [AddRightStrictMono α] {a b : α} (h : a < b) (c : α) : c - b < c - a
• sub_lt_sub_iff_left 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] [AddRightStrictMono α] {b c : α} (a : α) : a - b < a - c ↔ c < b
• StrictAntiOn.neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α] [Preorder β] {f : β → α} {s : Set β} (hf : StrictAntiOn f s) : StrictMonoOn (fun x => -f x) s
• StrictMonoOn.neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α] [Preorder β] {f : β → α} {s : Set β} (hf : StrictMonoOn f s) : StrictAntiOn (fun x => -f x) s
• add_neg_neg_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} : b + -a < 0 ↔ b < a
• lt_add_neg_iff_lt 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} : 0 < a + -b ↔ b < a
• lt_neg_iff_add_neg 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} : a < -b ↔ a + b < 0
• neg_add_neg_iff_lt 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} : a + -b < 0 ↔ a < b
• neg_lt_iff_pos_add 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b : α} : -a < b ↔ 0 < b + a
• add_neg_lt_iff_lt_add 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b c : α} : a + -b < c ↔ a < c + b
• lt_add_neg_iff_add_lt 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddRightStrictMono α] {a b c : α} : c < a + -b ↔ c + b < a
• neg_lt_sub_iff_lt_add 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] [AddRightStrictMono α] {a b c : α} : -a < b - c ↔ c < a + b
• add_neg_lt_neg_add_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
  {α : Type u} [AddGroup α] [LT α] [AddLeftStrictMono α] {a b c d : α} [AddRightStrictMono α] : a + -b < -d + c ↔ d + a < c + b
• lt_one_add 📋 Mathlib.Algebra.Order.Monoid.NatCast
  {α : Type u_1} [One α] [AddZeroClass α] [PartialOrder α] [ZeroLEOneClass α] [NeZero 1] [AddRightStrictMono α] (a : α) : a < 1 + a
• le_or_le_of_add_le_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
  {α : Type u_1} [LinearOrder α] [Add α] [AddLeftStrictMono α] [AddRightStrictMono α] {a₁ a₂ b₁ b₂ : α} : a₁ + b₁ ≤ a₂ + b₂ → a₁ ≤ a₂ ∨ b₁ ≤ b₂
• le_or_lt_of_add_le_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
  {α : Type u_1} [LinearOrder α] [Add α] [AddLeftMono α] [AddRightStrictMono α] {a₁ a₂ b₁ b₂ : α} : a₁ + b₁ ≤ a₂ + b₂ → a₁ ≤ a₂ ∨ b₁ < b₂
• add_lt_add_iff_of_le_of_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
  {α : Type u_1} [LinearOrder α] [Add α] [AddLeftMono α] [AddRightMono α] [AddLeftStrictMono α] [AddRightStrictMono α] {a₁ a₂ b₁ b₂ : α} (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) : a₁ + b₁ < a₂ + b₂ ↔ a₁ < a₂ ∨ b₁ < b₂
• strictAnti_mul_left 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
  {R : Type u} [Semiring R] [PartialOrder R] [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] {a : R} (ha : a < 0) : StrictAnti fun x => a * x
• strictAnti_mul_right 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
  {R : Type u} [Semiring R] [PartialOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] {a : R} (ha : a < 0) : StrictAnti fun x => x * a
• StrictAnti.const_mul_of_neg 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
  {R : Type u} {α : Type u_1} [Semiring R] [PartialOrder R] {a : R} [Preorder α] {f : α → R} [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (hf : StrictAnti f) (ha : a < 0) : StrictMono fun x => a * f x
• StrictAnti.mul_const_of_neg 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
  {R : Type u} {α : Type u_1} [Semiring R] [PartialOrder R] {a : R} [Preorder α] {f : α → R} [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (hf : StrictAnti f) (ha : a < 0) : StrictMono fun x => f x * a
• StrictMono.const_mul_of_neg 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
  {R : Type u} {α : Type u_1} [Semiring R] [PartialOrder R] {a : R} [Preorder α] {f : α → R} [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (hf : StrictMono f) (ha : a < 0) : StrictAnti fun x => a * f x
• StrictMono.mul_const_of_neg 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
  {R : Type u} {α : Type u_1} [Semiring R] [PartialOrder R] {a : R} [Preorder α] {f : α → R} [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (hf : StrictMono f) (ha : a < 0) : StrictAnti fun x => f x * a
• lt_mul_of_lt_one_left 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
  {R : Type u} [Semiring R] [PartialOrder R] {a b : R} [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (hb : b < 0) (h : a < 1) : b < a * b
• lt_mul_of_lt_one_right 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
  {R : Type u} [Semiring R] [PartialOrder R] {a b : R} [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (ha : a < 0) (h : b < 1) : a < a * b
• mul_lt_mul_of_neg_left 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
  {R : Type u} [Semiring R] [PartialOrder R] {a b c : R} [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (h : b < a) (hc : c < 0) : c * a < c * b
• mul_lt_mul_of_neg_right 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
  {R : Type u} [Semiring R] [PartialOrder R] {a b c : R} [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (h : b < a) (hc : c < 0) : a * c < b * c
• mul_lt_of_one_lt_left 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
  {R : Type u} [Semiring R] [PartialOrder R] {a b : R} [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (hb : b < 0) (h : 1 < a) : a * b < b
• mul_lt_of_one_lt_right 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
  {R : Type u} [Semiring R] [PartialOrder R] {a b : R} [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (ha : a < 0) (h : 1 < b) : a * b < a
• mul_pos_of_neg_of_neg 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
  {R : Type u} [Semiring R] [PartialOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] {a b : R} (ha : a < 0) (hb : b < 0) : 0 < a * b
• mul_lt_mul_left_of_neg 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
  {R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] {a b c : R} (h : c < 0) : c * a < c * b ↔ b < a
• mul_lt_mul_right_of_neg 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
  {R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] {a b c : R} (h : c < 0) : a * c < b * c ↔ b < a
• cmp_mul_neg_left 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
  {R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightReflectLT R] [AddRightStrictMono R] {a : R} (ha : a < 0) (b c : R) : cmp (a * b) (a * c) = cmp c b
• cmp_mul_neg_right 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
  {R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightReflectLT R] [AddRightStrictMono R] {a : R} (ha : a < 0) (b c : R) : cmp (b * a) (c * a) = cmp c b
• OrderDual.addRightStrictMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
  {α : Type u} [LT α] [Add α] [c : AddRightStrictMono α] : AddRightStrictMono αᵒᵈ
• instIsAddTorsionFreeOfAddLeftStrictMonoOfAddRightStrictMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
  {M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftStrictMono M] [AddRightStrictMono M] : IsAddTorsionFree M
• nsmul_right_strictMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
  {M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddRightStrictMono M] {n : ℕ} (hn : n ≠ 0) : StrictMono fun x => n • x
• StrictMono.const_nsmul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
  {β : Type u_1} {M : Type u_3} [AddMonoid M] [Preorder M] [Preorder β] [AddLeftStrictMono M] [AddRightStrictMono M] {f : β → M} (hf : StrictMono f) {n : ℕ} : n ≠ 0 → StrictMono fun x => n • f x
• nsmul_lt_nsmul_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
  {M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddRightStrictMono M] {n : ℕ} (hn : n ≠ 0) {a b : M} (hab : a < b) : n • a < n • b
• Right.nsmul_neg_iff 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
  {M : Type u_3} [AddMonoid M] [LinearOrder M] [AddRightStrictMono M] {n : ℕ} {x : M} (hn : 0 < n) : n • x < 0 ↔ x < 0
• le_of_nsmul_le_nsmul_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
  {M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftStrictMono M] [AddRightStrictMono M] {a b : M} {n : ℕ} (hn : n ≠ 0) : n • a ≤ n • b → a ≤ b
• nsmul_le_nsmul_iff_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
  {M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftStrictMono M] [AddRightStrictMono M] {a b : M} {n : ℕ} (hn : n ≠ 0) : n • a ≤ n • b ↔ a ≤ b
• le_max_of_two_nsmul_le_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
  {M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftStrictMono M] [AddRightStrictMono M] {a b c : M} (h : 2 • a ≤ b + c) : a ≤ max b c
• min_le_of_add_le_two_nsmul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
  {M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftStrictMono M] [AddRightStrictMono M] {a b c : M} (h : a + b ≤ 2 • c) : min a b ≤ c
• WithBot.add_lt_add_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
  {α : Type u} [Add α] {x y z : WithBot α} [LT α] [AddRightStrictMono α] (hz : z ≠ ⊥) : x < y → x + z < y + z
• WithTop.add_lt_add_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
  {α : Type u} [Add α] {x y z : WithTop α} [LT α] [AddRightStrictMono α] (hz : z ≠ ⊤) : x < y → x + z < y + z
• WithBot.add_lt_add_iff_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
  {α : Type u} [Add α] {x y z : WithBot α} [LT α] [AddRightStrictMono α] [AddRightReflectLT α] (hz : z ≠ ⊥) : x + z < y + z ↔ x < y
• WithTop.add_lt_add_iff_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
  {α : Type u} [Add α] {x y z : WithTop α} [LT α] [AddRightStrictMono α] [AddRightReflectLT α] (hz : z ≠ ⊤) : x + z < y + z ↔ x < y
• WithTop.add_lt_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
  {α : Type u} [Add α] {w x y z : WithTop α} [Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α] (xz : x < z) (yw : y < w) : x + y < z + w
• WithBot.add_lt_add_of_lt_of_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
  {α : Type u} [Add α] {w x y z : WithBot α} [Preorder α] [AddLeftMono α] [AddRightStrictMono α] (hx : x ≠ ⊥) (hwy : w < y) (hxz : x ≤ z) : w + x < y + z
• WithTop.add_lt_add_of_lt_of_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
  {α : Type u} [Add α] {w x y z : WithTop α} [Preorder α] [AddLeftMono α] [AddRightStrictMono α] (hx : x ≠ ⊤) (hwy : w < y) (hxz : x ≤ z) : w + x < y + z
• OrderEmbedding.addRight 📋 Mathlib.Algebra.Order.Monoid.Basic
  {α : Type u_2} [Add α] [LinearOrder α] [AddRightStrictMono α] (m : α) : α ↪o α
• OrderEmbedding.addRight_apply 📋 Mathlib.Algebra.Order.Monoid.Basic
  {α : Type u_2} [Add α] [LinearOrder α] [AddRightStrictMono α] (m n : α) : (OrderEmbedding.addRight m) n = n + m
• Positive.addRightStrictMono 📋 Mathlib.Algebra.Order.Positive.Ring
  {M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddRightStrictMono M] : AddRightStrictMono { x // 0 < x }
• List.sum_lt_sum_of_ne_nil 📋 Mathlib.Algebra.Order.BigOperators.Group.List
  {ι : Type u_1} {M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddLeftMono M] [AddRightStrictMono M] [AddRightMono M] {l : List ι} (hl : l ≠ []) (f g : ι → M) (hlt : ∀ i ∈ l, f i < g i) : (List.map f l).sum < (List.map g l).sum
• List.sum_lt_sum 📋 Mathlib.Algebra.Order.BigOperators.Group.List
  {ι : Type u_1} {M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddLeftMono M] [AddRightStrictMono M] [AddRightMono M] {l : List ι} (f g : ι → M) (h₁ : ∀ i ∈ l, f i ≤ g i) (h₂ : ∃ i ∈ l, f i < g i) : (List.map f l).sum < (List.map g l).sum
• List.exists_le_of_sum_le 📋 Mathlib.Algebra.Order.BigOperators.Group.List
  {ι : Type u_1} {M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftStrictMono M] [AddLeftMono M] [AddRightStrictMono M] [AddRightMono M] {l : List ι} (hl : l ≠ []) (f g : ι → M) (h : (List.map f l).sum ≤ (List.map g l).sum) : ∃ x ∈ l, f x ≤ g x
• TwoUniqueSums.of_covariant_left 📋 Mathlib.Algebra.Group.UniqueProds.Basic
  {G : Type u} [Add G] [IsLeftCancelAdd G] [LinearOrder G] [AddRightStrictMono G] : TwoUniqueSums G
• AddMonoidAlgebra.Monic.mul 📋 Mathlib.Algebra.MonoidAlgebra.Degree
  {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) (hp : AddMonoidAlgebra.Monic D p) (hq : AddMonoidAlgebra.Monic D q) : AddMonoidAlgebra.Monic D (p * q)
• AddMonoidAlgebra.Monic.leadingCoeff_mul_eq_left 📋 Mathlib.Algebra.MonoidAlgebra.Degree
  {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) (hq : AddMonoidAlgebra.Monic D q) : AddMonoidAlgebra.leadingCoeff D (p * q) = AddMonoidAlgebra.leadingCoeff D p
• AddMonoidAlgebra.Monic.leadingCoeff_mul_eq_right 📋 Mathlib.Algebra.MonoidAlgebra.Degree
  {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) (hp : AddMonoidAlgebra.Monic D p) : AddMonoidAlgebra.leadingCoeff D (p * q) = AddMonoidAlgebra.leadingCoeff D q
• AddMonoidAlgebra.Monic.pow 📋 Mathlib.Algebra.MonoidAlgebra.Degree
  {R : Type u_1} [Semiring R] {A : Type u_8} {B : Type u_9} [AddMonoid A] [AddMonoid B] [LinearOrder B] [OrderBot B] [AddLeftStrictMono B] [AddRightStrictMono B] {D : A → B} {p : AddMonoidAlgebra R A} {n : ℕ} (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) (hD : Function.Injective D) (hp : AddMonoidAlgebra.Monic D p) : AddMonoidAlgebra.Monic D (p ^ n)
• AddMonoidAlgebra.leadingCoeff_mul 📋 Mathlib.Algebra.MonoidAlgebra.Degree
  {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] [NoZeroDivisors R] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) : AddMonoidAlgebra.leadingCoeff D (p * q) = AddMonoidAlgebra.leadingCoeff D p * AddMonoidAlgebra.leadingCoeff D q
• AddMonoidAlgebra.Monic.supDegree_mul_of_ne_zero_left 📋 Mathlib.Algebra.MonoidAlgebra.Degree
  {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) (hq : AddMonoidAlgebra.Monic D q) (hp : p ≠ 0) : AddMonoidAlgebra.supDegree D (p * q) = AddMonoidAlgebra.supDegree D p + AddMonoidAlgebra.supDegree D q
• AddMonoidAlgebra.Monic.supDegree_mul_of_ne_zero_right 📋 Mathlib.Algebra.MonoidAlgebra.Degree
  {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) (hp : AddMonoidAlgebra.Monic D p) (hq : q ≠ 0) : AddMonoidAlgebra.supDegree D (p * q) = AddMonoidAlgebra.supDegree D p + AddMonoidAlgebra.supDegree D q
• AddMonoidAlgebra.Monic.supDegree_pow 📋 Mathlib.Algebra.MonoidAlgebra.Degree
  {R : Type u_1} [Semiring R] {A : Type u_8} {B : Type u_9} [AddMonoid A] [AddMonoid B] [LinearOrder B] [OrderBot B] [AddLeftStrictMono B] [AddRightStrictMono B] {D : A → B} {p : AddMonoidAlgebra R A} {n : ℕ} (hzero : D 0 = 0) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) (hD : Function.Injective D) [Nontrivial R] (hp : AddMonoidAlgebra.Monic D p) : AddMonoidAlgebra.supDegree D (p ^ n) = n • AddMonoidAlgebra.supDegree D p
• AddMonoidAlgebra.apply_supDegree_add_supDegree 📋 Mathlib.Algebra.MonoidAlgebra.Degree
  {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) : (p * q).coeff (Function.invFun D (AddMonoidAlgebra.supDegree D p + AddMonoidAlgebra.supDegree D q)) = AddMonoidAlgebra.leadingCoeff D p * AddMonoidAlgebra.leadingCoeff D q
• AddMonoidAlgebra.coeff_supDegree_add_supDegree 📋 Mathlib.Algebra.MonoidAlgebra.Degree
  {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) : (p * q).coeff (Function.invFun D (AddMonoidAlgebra.supDegree D p + AddMonoidAlgebra.supDegree D q)) = AddMonoidAlgebra.leadingCoeff D p * AddMonoidAlgebra.leadingCoeff D q
• AddMonoidAlgebra.apply_add_of_supDegree_le 📋 Mathlib.Algebra.MonoidAlgebra.Degree
  {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [SemilatticeSup B] [OrderBot B] {D : A → B} {p q : AddMonoidAlgebra R A} [AddZeroClass A] [Add B] (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) {ap aq : A} (hp : AddMonoidAlgebra.supDegree D p ≤ D ap) (hq : AddMonoidAlgebra.supDegree D q ≤ D aq) : (p * q).coeff (ap + aq) = p.coeff ap * q.coeff aq
• AddMonoidAlgebra.coeff_add_of_supDegree_le 📋 Mathlib.Algebra.MonoidAlgebra.Degree
  {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [SemilatticeSup B] [OrderBot B] {D : A → B} {p q : AddMonoidAlgebra R A} [AddZeroClass A] [Add B] (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) {ap aq : A} (hp : AddMonoidAlgebra.supDegree D p ≤ D ap) (hq : AddMonoidAlgebra.supDegree D q ≤ D aq) : (p * q).coeff (ap + aq) = p.coeff ap * q.coeff aq
• AddMonoidAlgebra.Monic.supDegree_mul 📋 Mathlib.Algebra.MonoidAlgebra.Degree
  {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) (hbot : ⊥ + ⊥ = ⊥) (hp : AddMonoidAlgebra.Monic D p) (hq : AddMonoidAlgebra.Monic D q) : AddMonoidAlgebra.supDegree D (p * q) = AddMonoidAlgebra.supDegree D p + AddMonoidAlgebra.supDegree D q
• AddMonoidAlgebra.supDegree_mul 📋 Mathlib.Algebra.MonoidAlgebra.Degree
  {R : Type u_1} {A : Type u_3} {B : Type u_5} [Semiring R] [LinearOrder B] [OrderBot B] {p q : AddMonoidAlgebra R A} {D : A → B} [AddZeroClass A] [Add B] [AddLeftStrictMono B] [AddRightStrictMono B] (hD : Function.Injective D) (hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) (hpq : AddMonoidAlgebra.leadingCoeff D p * AddMonoidAlgebra.leadingCoeff D q ≠ 0) (hp : p ≠ 0) (hq : q ≠ 0) : AddMonoidAlgebra.supDegree D (p * q) = AddMonoidAlgebra.supDegree D p + AddMonoidAlgebra.supDegree D q
• DFinsupp.Colex.addRightStrictMono 📋 Mathlib.Data.DFinsupp.Lex
  {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), AddRightStrictMono (α i)] : AddRightStrictMono (Colex (Π₀ (i : ι), α i))
• DFinsupp.Lex.addRightStrictMono 📋 Mathlib.Data.DFinsupp.Lex
  {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), AddRightStrictMono (α i)] : AddRightStrictMono (Lex (Π₀ (i : ι), α i))
• DFinsupp.Colex.addRightMono 📋 Mathlib.Data.DFinsupp.Lex
  {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), AddRightStrictMono (α i)] : AddRightMono (Colex (Π₀ (i : ι), α i))
• DFinsupp.Lex.addRightMono 📋 Mathlib.Data.DFinsupp.Lex
  {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → AddMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), AddRightStrictMono (α i)] : AddRightMono (Lex (Π₀ (i : ι), α i))
• Finsupp.Colex.addRightStrictMono 📋 Mathlib.Data.Finsupp.Lex
  {α : Type u_1} {N : Type u_2} [LinearOrder α] [AddMonoid N] [LinearOrder N] [AddRightStrictMono N] : AddRightStrictMono (Colex (α →₀ N))
• Finsupp.Lex.addRightStrictMono 📋 Mathlib.Data.Finsupp.Lex
  {α : Type u_1} {N : Type u_2} [LinearOrder α] [AddMonoid N] [LinearOrder N] [AddRightStrictMono N] : AddRightStrictMono (Lex (α →₀ N))
• Finsupp.Colex.addRightMono 📋 Mathlib.Data.Finsupp.Lex
  {α : Type u_1} {N : Type u_2} [LinearOrder α] [AddMonoid N] [LinearOrder N] [AddRightStrictMono N] : AddRightMono (Colex (α →₀ N))
• Finsupp.Lex.addRightMono 📋 Mathlib.Data.Finsupp.Lex
  {α : Type u_1} {N : Type u_2} [LinearOrder α] [AddMonoid N] [LinearOrder N] [AddRightStrictMono N] : AddRightMono (Lex (α →₀ N))
• Set.Ici_add_Ioi_subset 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
  {α : Type u_1} [Add α] [PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] (a b : α) : Set.Ici a + Set.Ioi b ⊆ Set.Ioi (a + b)
• Set.Iic_add_Iio_subset 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
  {α : Type u_1} [Add α] [PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] (a b : α) : Set.Iic a + Set.Iio b ⊆ Set.Iio (a + b)
• Set.Iio_add_Iic_subset 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
  {α : Type u_1} [Add α] [PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] (a b : α) : Set.Iio a + Set.Iic b ⊆ Set.Iio (a + b)
• Set.Ioi_add_Ici_subset 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
  {α : Type u_1} [Add α] [PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] (a b : α) : Set.Ioi a + Set.Ici b ⊆ Set.Ioi (a + b)
• Set.Icc_add_Ico_subset 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
  {α : Type u_1} [Add α] [PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] (a b c d : α) : Set.Icc a b + Set.Ico c d ⊆ Set.Ico (a + c) (b + d)
• Set.Ico_add_Icc_subset 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
  {α : Type u_1} [Add α] [PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] (a b c d : α) : Set.Ico a b + Set.Icc c d ⊆ Set.Ico (a + c) (b + d)
• Set.Ico_add_Ioc_subset 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
  {α : Type u_1} [Add α] [PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] (a b c d : α) : Set.Ico a b + Set.Ioc c d ⊆ Set.Ioo (a + c) (b + d)
• Set.Ioc_add_Ico_subset 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
  {α : Type u_1} [Add α] [PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] (a b c d : α) : Set.Ioc a b + Set.Ico c d ⊆ Set.Ioo (a + c) (b + d)
• Finset.Ici_add_Ioi_subset 📋 Mathlib.Algebra.Group.Pointwise.Finset.Interval
  {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [AddLeftStrictMono α] [AddRightStrictMono α] [LocallyFiniteOrderTop α] (a b : α) : Finset.Ici a + Finset.Ioi b ⊆ Finset.Ioi (a + b)
• Finset.Iic_add_Iio_subset 📋 Mathlib.Algebra.Group.Pointwise.Finset.Interval
  {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [AddLeftStrictMono α] [AddRightStrictMono α] [LocallyFiniteOrderBot α] (a b : α) : Finset.Iic a + Finset.Iio b ⊆ Finset.Iio (a + b)
• Finset.Iio_add_Iic_subset 📋 Mathlib.Algebra.Group.Pointwise.Finset.Interval
  {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [AddLeftStrictMono α] [AddRightStrictMono α] [LocallyFiniteOrderBot α] (a b : α) : Finset.Iio a + Finset.Iic b ⊆ Finset.Iio (a + b)
• Finset.Ioi_add_Ici_subset 📋 Mathlib.Algebra.Group.Pointwise.Finset.Interval
  {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [AddLeftStrictMono α] [AddRightStrictMono α] [LocallyFiniteOrderTop α] (a b : α) : Finset.Ioi a + Finset.Ici b ⊆ Finset.Ioi (a + b)
• Finset.Icc_add_Ico_subset 📋 Mathlib.Algebra.Group.Pointwise.Finset.Interval
  {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [AddLeftStrictMono α] [AddRightStrictMono α] [LocallyFiniteOrder α] (a b c d : α) : Finset.Icc a b + Finset.Ico c d ⊆ Finset.Ico (a + c) (b + d)
• Finset.Ico_add_Icc_subset 📋 Mathlib.Algebra.Group.Pointwise.Finset.Interval
  {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [AddLeftStrictMono α] [AddRightStrictMono α] [LocallyFiniteOrder α] (a b c d : α) : Finset.Ico a b + Finset.Icc c d ⊆ Finset.Ico (a + c) (b + d)
• Finset.Ico_add_Ioc_subset 📋 Mathlib.Algebra.Group.Pointwise.Finset.Interval
  {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [AddLeftStrictMono α] [AddRightStrictMono α] [LocallyFiniteOrder α] (a b c d : α) : Finset.Ico a b + Finset.Ioc c d ⊆ Finset.Ioo (a + c) (b + d)
• Finset.Ioc_add_Ico_subset 📋 Mathlib.Algebra.Group.Pointwise.Finset.Interval
  {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [AddLeftStrictMono α] [AddRightStrictMono α] [LocallyFiniteOrder α] (a b c d : α) : Finset.Ioc a b + Finset.Ico c d ⊆ Finset.Ioo (a + c) (b + d)
• lt_hasSum 📋 Mathlib.Topology.Algebra.InfiniteSum.Order
  {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [AddCommMonoid α] [Preorder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} [L.NeBot] [L.LeAtTop] [AddRightStrictMono α] (hf : HasSum f a L) (i : ι) (hi : ∀ (j : ι), j ≠ i → 0 ≤ f j) (j : ι) (hij : j ≠ i) (hj : 0 < f j) : f i < a
• Right.sign_neg 📋 Mathlib.Basic.Sign.Defs
  {α : Type u_1} [AddGroup α] [Preorder α] [DecidableLT α] [AddRightStrictMono α] (a : α) : SignType.sign (-a) = -SignType.sign a
• StrictConvex.smul_mem_of_zero_mem 📋 Mathlib.Analysis.Convex.Strict
  {𝕜 : Type u_1} {E : Type u_3} [Ring 𝕜] [PartialOrder 𝕜] [TopologicalSpace E] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {x : E} [AddRightStrictMono 𝕜] (hs : StrictConvex 𝕜 s) (zero_mem : 0 ∈ s) (hx : x ∈ s) (hx₀ : x ≠ 0) {t : 𝕜} (ht₀ : 0 < t) (ht₁ : t < 1) : t • x ∈ interior s
• StrictConvex.add_smul_mem 📋 Mathlib.Analysis.Convex.Strict
  {𝕜 : Type u_1} {E : Type u_3} [Ring 𝕜] [PartialOrder 𝕜] [TopologicalSpace E] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {x y : E} [AddRightStrictMono 𝕜] (hs : StrictConvex 𝕜 s) (hx : x ∈ s) (hxy : x + y ∈ s) (hy : y ≠ 0) {t : 𝕜} (ht₀ : 0 < t) (ht₁ : t < 1) : x + t • y ∈ interior s
• Set.AddAntidiagonal.finite_of_isPWO 📋 Mathlib.Data.Set.MulAntidiagonal
  {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsCancelAdd α] [AddLeftMono α] [AddRightStrictMono α] {s t : Set α} (hs : s.IsPWO) (ht : t.IsPWO) (a : α) : (s.antidiagonal t a).Finite
• Set.AddAntidiagonal.finite_of_isWF 📋 Mathlib.Data.Set.MulAntidiagonal
  {α : Type u_1} [AddCancelCommMonoid α] [LinearOrder α] [AddLeftMono α] [AddRightStrictMono α] {s t : Set α} (hs : s.IsWF) (ht : t.IsWF) (a : α) : (s.antidiagonal t a).Finite
• Set.AddAntidiagonal.eq_of_fst_le_fst_of_snd_le_snd 📋 Mathlib.Data.Set.MulAntidiagonal
  {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsCancelAdd α] [AddLeftMono α] [AddRightStrictMono α] (s t : Set α) (a : α) {x y : ↑(s.antidiagonal t a)} (h₁ : (↑x).1 ≤ (↑y).1) (h₂ : (↑x).2 ≤ (↑y).2) : x = y
• Tropical.mulRightStrictMono 📋 Mathlib.Algebra.Tropical.Basic
  {R : Type u} [Preorder R] [Add R] [AddRightStrictMono R] : MulRightStrictMono (Tropical R)

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