Loogle!
Result
Found 286 declarations mentioning MulRightMono. Of these, only the first 200 are shown.
- MulRightMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
(M : Type u_1) [Mul M] [LE M] : Prop - mulRightMono_of_mulLeftMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
(N : Type u_2) [CommSemigroup N] [LE N] [MulLeftMono N] : MulRightMono N - mulRightMono_of_mulRightStrictMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
(M : Type u_3) [Mul M] [PartialOrder M] [MulRightStrictMono M] : MulRightMono M - IsRightCancelMul.mulRightStrictMono_of_mulRightMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
(N : Type u_2) [Mul N] [IsRightCancelMul N] [PartialOrder N] [MulRightMono N] : MulRightStrictMono N - mulRightReflectLT_of_mulRightMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
(N : Type u_2) [Mul N] [LinearOrder N] [MulRightMono N] : MulRightReflectLT N - Group.mulRightReflectLE_of_mulRightMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
{N : Type u_2} [Group N] [LE N] [MulRightMono N] : MulRightReflectLE N - mul_left_mono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a : α} [Mul α] [Preorder α] [MulRightMono α] : Monotone fun x => x * a - mul_le_mul_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {b c : α} [Mul α] [LE α] [i : MulRightMono α] (bc : b ≤ c) (a : α) : b * a ≤ c * a - Antitone.mul_const' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : β → α} [MulRightMono α] (hf : Antitone f) (a : α) : Antitone fun x => f x * a - Monotone.mul_const' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : β → α} [MulRightMono α] (hf : Monotone f) (a : α) : Monotone fun x => f x * a - mulRightStrictMono_iff_mulRightMono_and_isRightCancelMul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [Mul α] [LinearOrder α] : MulRightStrictMono α ↔ MulRightMono α ∧ IsRightCancelMul α - mul_le_mul_iff_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {b c : α} [Mul α] [LE α] [MulRightMono α] [MulRightReflectLE α] (a : α) : b * a ≤ c * a ↔ b ≤ c - AntitoneOn.mul_const' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : β → α} {s : Set β} [MulRightMono α] (hf : AntitoneOn f s) (a : α) : AntitoneOn (fun x => f x * a) s - MonotoneOn.mul_const' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : β → α} {s : Set β} [MulRightMono α] (hf : MonotoneOn f s) (a : α) : MonotoneOn (fun x => f x * a) s - le_mul_of_one_le_left' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b : α} [MulOneClass α] [LE α] [MulRightMono α] (h : 1 ≤ b) : a ≤ b * a - mul_le_of_le_one_left' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b : α} [MulOneClass α] [LE α] [MulRightMono α] (h : b ≤ 1) : b * a ≤ a - le_mul_of_le_mul_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Mul α] [Preorder α] [MulRightMono α] (h : a ≤ b * c) (hle : b ≤ d) : a ≤ d * c - lt_mul_of_lt_mul_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Mul α] [Preorder α] [MulRightMono α] (h : a < b * c) (hle : b ≤ d) : a < d * c - mul_le_of_mul_le_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Mul α] [Preorder α] [MulRightMono α] (h : a * b ≤ c) (hle : d ≤ a) : d * b ≤ c - mul_lt_of_mul_lt_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Mul α] [Preorder α] [MulRightMono α] (h : a * b < c) (hle : d ≤ a) : d * b < c - Antitone.mul' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f g : β → α} [MulLeftMono α] [MulRightMono α] (hf : Antitone f) (hg : Antitone g) : Antitone fun x => f x * g x - Antitone.mul_strictAnti' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] [MulLeftStrictMono α] [MulRightMono α] {f g : β → α} (hf : Antitone f) (hg : StrictAnti g) : StrictAnti fun x => f x * g x - Monotone.mul' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f g : β → α} [MulLeftMono α] [MulRightMono α] (hf : Monotone f) (hg : Monotone g) : Monotone fun x => f x * g x - Monotone.mul_strictMono' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] [MulLeftStrictMono α] [MulRightMono α] {f g : β → α} (hf : Monotone f) (hg : StrictMono g) : StrictMono fun x => f x * g x - le_mul_iff_one_le_left' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {b : α} [MulOneClass α] [LE α] [MulRightMono α] [MulRightReflectLE α] (a : α) : a ≤ b * a ↔ 1 ≤ b - mul_le_iff_le_one_left' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b : α} [MulOneClass α] [LE α] [MulRightMono α] [MulRightReflectLE α] : a * b ≤ b ↔ a ≤ 1 - mul_le_mul' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Mul α] [Preorder α] [MulLeftMono α] [MulRightMono α] (h₁ : a ≤ b) (h₂ : c ≤ d) : a * c ≤ b * d - mul_lt_mul_of_le_of_lt 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Mul α] [Preorder α] [MulLeftStrictMono α] [MulRightMono α] (h₁ : a ≤ b) (h₂ : c < d) : a * c < b * d - AntitoneOn.mul' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f g : β → α} {s : Set β} [MulLeftMono α] [MulRightMono α] (hf : AntitoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (fun x => f x * g x) s - AntitoneOn.mul_strictAnti' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {s : Set β} [MulLeftStrictMono α] [MulRightMono α] {f g : β → α} (hf : AntitoneOn f s) (hg : StrictAntiOn g s) : StrictAntiOn (fun x => f x * g x) s - Left.mul_lt_mul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Mul α] [Preorder α] [MulLeftStrictMono α] [MulRightMono α] (h₁ : a < b) (h₂ : c < d) : a * c < b * d - MonotoneOn.mul' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f g : β → α} {s : Set β} [MulLeftMono α] [MulRightMono α] (hf : MonotoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun x => f x * g x) s - MonotoneOn.mul_strictMono' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {s : Set β} [MulLeftStrictMono α] [MulRightMono α] {f g : β → α} (hf : MonotoneOn f s) (hg : StrictMonoOn g s) : StrictMonoOn (fun x => f x * g x) s - le_mul_of_one_le_of_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulRightMono α] (ha : 1 ≤ a) (hbc : b ≤ c) : b ≤ a * c - le_of_le_mul_of_le_one_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulRightMono α] (h : a ≤ b * c) (hle : b ≤ 1) : a ≤ c - le_of_mul_le_of_one_le_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulRightMono α] (h : a * b ≤ c) (hle : 1 ≤ a) : b ≤ c - lt_mul_of_one_le_of_lt 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulRightMono α] (ha : 1 ≤ a) (hbc : b < c) : b < a * c - lt_mul_of_one_lt_of_lt' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulRightMono α] (ha : 1 < a) (hbc : b < c) : b < a * c - lt_of_lt_mul_of_le_one_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulRightMono α] (h : a < b * c) (hle : b ≤ 1) : a < c - lt_of_mul_lt_of_one_le_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulRightMono α] (h : a * b < c) (hle : 1 ≤ a) : b < c - mul_le_of_le_one_of_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulRightMono α] (ha : a ≤ 1) (hbc : b ≤ c) : a * b ≤ c - mul_lt_of_le_one_of_lt 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulRightMono α] (ha : a ≤ 1) (hbc : b < c) : a * b < c - mul_lt_of_lt_one_of_lt' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulRightMono α] (ha : a < 1) (hbc : b < c) : a * b < c - Right.mul_le_one 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulRightMono α] (ha : a ≤ 1) (hbc : b ≤ c) : a * b ≤ c - Right.mul_lt_one' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulRightMono α] (ha : a < 1) (hbc : b < c) : a * b < c - Right.mul_lt_one_of_le_of_lt 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulRightMono α] (ha : a ≤ 1) (hbc : b < c) : a * b < c - Right.one_le_mul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulRightMono α] (ha : 1 ≤ a) (hbc : b ≤ c) : b ≤ a * c - Right.one_lt_mul' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulRightMono α] (ha : 1 < a) (hbc : b < c) : b < a * c - Right.one_lt_mul_of_le_of_lt 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulRightMono α] (ha : 1 ≤ a) (hbc : b < c) : b < a * c - one_lt_mul_of_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [MulOneClass α] [Preorder α] [IsBotOneClass α] [MulRightMono α] {b : α} (hb : 1 < b) (a : α) : 1 < a * b - Right.one_lt_mul_of_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [MulOneClass α] [Preorder α] [IsBotOneClass α] [MulRightMono α] {b : α} (hb : 1 < b) (a : α) : 1 < a * b - max_mul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [Mul α] [LinearOrder α] [MulRightMono α] (a b c : α) : max a b * c = max (a * c) (b * c) - min_mul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [Mul α] [LinearOrder α] [MulRightMono α] (a b c : α) : min a b * c = min (a * c) (b * c) - mul_le_mul_three 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d e f : α} [Mul α] [Preorder α] [MulLeftMono α] [MulRightMono α] (h₁ : a ≤ d) (h₂ : b ≤ e) (h₃ : c ≤ f) : a * b * c ≤ d * e * f - eq_one_of_mul_le_one_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b : α} [MulOneClass α] [PartialOrder α] [MulRightMono α] (ha : 1 ≤ a) (hb : 1 ≤ b) (hab : a * b ≤ 1) : b = 1 - eq_one_of_one_le_mul_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b : α} [MulOneClass α] [PartialOrder α] [MulRightMono α] (ha : a ≤ 1) (hb : b ≤ 1) (hab : 1 ≤ a * b) : b = 1 - min_lt_max_of_mul_lt_mul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Mul α] [LinearOrder α] [MulLeftMono α] [MulRightMono α] (h : a * b < c * d) : min a b < max c d - Left.min_le_max_of_mul_le_mul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Mul α] [LinearOrder α] [MulLeftStrictMono α] [MulRightMono α] (h : a * b ≤ c * d) : min a b ≤ max c d - max_mul_mul_le_max_mul_max' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Mul α] [LinearOrder α] [MulLeftMono α] [MulRightMono α] : max (a * b) (c * d) ≤ max a c * max b d - min_mul_min_le_min_mul_mul' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Mul α] [LinearOrder α] [MulLeftMono α] [MulRightMono α] : min a c * min b d ≤ min (a * b) (c * d) - mul_eq_one_iff_of_one_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b : α} [MulOneClass α] [PartialOrder α] [MulLeftMono α] [MulRightMono α] (ha : 1 ≤ a) (hb : 1 ≤ b) : a * b = 1 ↔ a = 1 ∧ b = 1 - div_le_div_right' 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulRightMono α] {a b : α} (h : a ≤ b) (c : α) : a / c ≤ b / c - div_le_div_iff_right 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulRightMono α] {a b : α} (c : α) : a / c ≤ b / c ↔ a ≤ b - div_le_one' 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulRightMono α] {a b : α} : a / b ≤ 1 ↔ a ≤ b - one_le_div' 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulRightMono α] {a b : α} : 1 ≤ a / b ↔ b ≤ a - Right.inv_le_self 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [Preorder α] [MulRightMono α] {a : α} (h : 1 ≤ a) : a⁻¹ ≤ a - Right.self_le_inv 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [Preorder α] [MulRightMono α] {a : α} (h : a ≤ 1) : a ≤ a⁻¹ - div_le_iff_le_mul 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulRightMono α] {a b c : α} : a / c ≤ b ↔ a ≤ b * c - le_div_iff_mul_le 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulRightMono α] {a b c : α} : a ≤ c / b ↔ a * b ≤ c - Antitone.inv 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} {β : Type u_1} [Group α] [Preorder α] [MulLeftMono α] [MulRightMono α] [Preorder β] {f : β → α} (hf : Antitone f) : Monotone fun x => (f x)⁻¹ - Monotone.inv 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} {β : Type u_1} [Group α] [Preorder α] [MulLeftMono α] [MulRightMono α] [Preorder β] {f : β → α} (hf : Monotone f) : Antitone fun x => (f x)⁻¹ - inv_le_inv_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulLeftMono α] {a b : α} [MulRightMono α] : a⁻¹ ≤ b⁻¹ ↔ b ≤ a - Right.inv_le_one_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulRightMono α] {a : α} : a⁻¹ ≤ 1 ↔ 1 ≤ a - Right.one_le_inv_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulRightMono α] {a : α} : 1 ≤ a⁻¹ ↔ a ≤ 1 - div_le_div_left' 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulLeftMono α] [MulRightMono α] {a b : α} (h : a ≤ b) (c : α) : c / b ≤ c / a - div_le_div_iff_left 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulLeftMono α] [MulRightMono α] {b c : α} (a : α) : a / b ≤ a / c ↔ c ≤ b - AntitoneOn.inv 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} {β : Type u_1} [Group α] [Preorder α] [MulLeftMono α] [MulRightMono α] [Preorder β] {f : β → α} {s : Set β} (hf : AntitoneOn f s) : MonotoneOn (fun x => (f x)⁻¹) s - MonotoneOn.inv 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} {β : Type u_1} [Group α] [Preorder α] [MulLeftMono α] [MulRightMono α] [Preorder β] {f : β → α} {s : Set β} (hf : MonotoneOn f s) : AntitoneOn (fun x => (f x)⁻¹) s - inv_le_iff_one_le_mul 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulRightMono α] {a b : α} : a⁻¹ ≤ b ↔ 1 ≤ b * a - le_inv_iff_mul_le_one_right 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulRightMono α] {a b : α} : a ≤ b⁻¹ ↔ a * b ≤ 1 - le_mul_inv_iff_le 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulRightMono α] {a b : α} : 1 ≤ a * b⁻¹ ↔ b ≤ a - mul_inv_le_one_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulRightMono α] {a b : α} : b * a⁻¹ ≤ 1 ↔ b ≤ a - mul_inv_le_one_iff_le 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulRightMono α] {a b : α} : a * b⁻¹ ≤ 1 ↔ a ≤ b - le_mul_inv_iff_mul_le 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulRightMono α] {a b c : α} : c ≤ a * b⁻¹ ↔ c * b ≤ a - mul_inv_le_iff_le_mul 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulRightMono α] {a b c : α} : a * b⁻¹ ≤ c ↔ a ≤ c * b - cmp_div_one' 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LinearOrder α] [MulRightMono α] (a b : α) : cmp (a / b) 1 = cmp a b - div_le_inv_mul_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LinearOrder α] [MulLeftMono α] {a b : α} [MulRightMono α] : a / b ≤ a⁻¹ * b ↔ a ≤ b - mul_inv_le_inv_mul_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulLeftMono α] {a b c d : α} [MulRightMono α] : a * b⁻¹ ≤ d⁻¹ * c ↔ d * a ≤ c * b - MulRightMono.toMulPosMono 📋 Mathlib.Algebra.Order.GroupWithZero.Defs
{α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulRightMono α] : MulPosMono α - max_mul_mul_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
{α : Type u_1} [LinearOrder α] [Mul α] [MulRightMono α] (a b c : α) : max (a * c) (b * c) = max a b * c - min_mul_mul_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
{α : Type u_1} [LinearOrder α] [Mul α] [MulRightMono α] (a b c : α) : min (a * c) (b * c) = min a b * c - min_le_mul_of_one_le_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
{α : Type u_1} [LinearOrder α] [MulOneClass α] [MulRightMono α] {a b : α} (ha : 1 ≤ a) : min a b ≤ a * b - lt_or_le_of_mul_le_mul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
{α : Type u_1} [LinearOrder α] [Mul α] [MulLeftStrictMono α] [MulRightMono α] {a₁ a₂ b₁ b₂ : α} : a₁ * b₁ ≤ a₂ * b₂ → a₁ < a₂ ∨ b₁ ≤ b₂ - lt_or_lt_of_mul_lt_mul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
{α : Type u_1} [LinearOrder α] [Mul α] [MulLeftMono α] [MulRightMono α] {a₁ a₂ b₁ b₂ : α} : a₁ * b₁ < a₂ * b₂ → a₁ < a₂ ∨ b₁ < b₂ - max_le_mul_of_one_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
{α : Type u_1} [LinearOrder α] [MulOneClass α] [MulLeftMono α] [MulRightMono α] {a b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) : max a b ≤ a * b - mul_lt_mul_iff_of_le_of_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
{α : Type u_1} [LinearOrder α] [Mul α] [MulLeftMono α] [MulRightMono α] [MulLeftStrictMono α] [MulRightStrictMono α] {a₁ a₂ b₁ b₂ : α} (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) : a₁ * b₁ < a₂ * b₂ ↔ a₁ < a₂ ∨ b₁ < b₂ - IsOrderedMonoid.toMulRightMono 📋 Mathlib.Algebra.Order.Monoid.Defs
{α : Type u_1} [CommMonoid α] [Preorder α] [IsOrderedMonoid α] : MulRightMono α - OrderIso.divRight 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [Group α] [LE α] [MulRightMono α] (a : α) : α ≃o α - OrderIso.mulRight 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [Group α] [LE α] [MulRightMono α] (a : α) : α ≃o α - OrderIso.inv 📋 Mathlib.Algebra.Order.Group.OrderIso
(α : Type u) [Group α] [LE α] [MulLeftMono α] [MulRightMono α] : α ≃o αᵒᵈ - OrderIso.divLeft 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [Group α] [LE α] [MulLeftMono α] [MulRightMono α] (a : α) : α ≃o αᵒᵈ - OrderIso.mulRight_toEquiv 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [Group α] [LE α] [MulRightMono α] (a : α) : (OrderIso.mulRight a).toEquiv = Equiv.mulRight a - OrderIso.mulRight_symm 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [Group α] [LE α] [MulRightMono α] (a : α) : (OrderIso.mulRight a).symm = OrderIso.mulRight a⁻¹ - inv_le_of_inv_le' 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [Group α] [LE α] [MulLeftMono α] [MulRightMono α] {a b : α} : a⁻¹ ≤ b → b⁻¹ ≤ a - le_inv_of_le_inv 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [Group α] [LE α] [MulLeftMono α] [MulRightMono α] {a b : α} : a ≤ b⁻¹ → b ≤ a⁻¹ - inv_le' 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [Group α] [LE α] [MulLeftMono α] [MulRightMono α] {a b : α} : a⁻¹ ≤ b ↔ b⁻¹ ≤ a - le_inv' 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [Group α] [LE α] [MulLeftMono α] [MulRightMono α] {a b : α} : a ≤ b⁻¹ ↔ b ≤ a⁻¹ - OrderIso.divRight_apply 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [Group α] [LE α] [MulRightMono α] (a b : α) : (OrderIso.divRight a) b = b / a - OrderIso.mulRight_apply 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [Group α] [LE α] [MulRightMono α] (a x : α) : (OrderIso.mulRight a) x = x * a - OrderIso.divRight_symm_apply 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [Group α] [LE α] [MulRightMono α] (a b : α) : (RelIso.symm (OrderIso.divRight a)) b = b * a - OrderIso.inv_apply 📋 Mathlib.Algebra.Order.Group.OrderIso
(α : Type u) [Group α] [LE α] [MulLeftMono α] [MulRightMono α] (a✝ : α) : (OrderIso.inv α) a✝ = OrderDual.toDual a✝⁻¹ - OrderIso.divLeft_apply 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [Group α] [LE α] [MulLeftMono α] [MulRightMono α] (a a✝ : α) : (OrderIso.divLeft a) a✝ = OrderDual.toDual (a / a✝) - OrderIso.inv_symm_apply 📋 Mathlib.Algebra.Order.Group.OrderIso
(α : Type u) [Group α] [LE α] [MulLeftMono α] [MulRightMono α] (a✝ : αᵒᵈ) : (RelIso.symm (OrderIso.inv α)) a✝ = (OrderDual.ofDual a✝)⁻¹ - OrderIso.divLeft_symm_apply 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [Group α] [LE α] [MulLeftMono α] [MulRightMono α] (a : α) (a✝ : αᵒᵈ) : (RelIso.symm (OrderIso.divLeft a)) a✝ = (OrderDual.ofDual a✝)⁻¹ * a - OrderDual.mulRightMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
{α : Type u} [LE α] [Mul α] [c : MulRightMono α] : MulRightMono αᵒᵈ - pow_left_mono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] [MulRightMono M] (n : ℕ) : Monotone fun a => a ^ n - Monotone.pow_const 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{β : Type u_1} {M : Type u_3} [Monoid M] [Preorder M] [Preorder β] [MulLeftMono M] [MulRightMono M] {f : β → M} (hf : Monotone f) (n : ℕ) : Monotone fun a => f a ^ n - Right.one_le_pow_of_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [Monoid M] [Preorder M] [MulRightMono M] {x : M} (hx : 1 ≤ x) {n : ℕ} : 1 ≤ x ^ n - Right.pow_le_one_of_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [Monoid M] [Preorder M] [MulRightMono M] {x : M} (hx : x ≤ 1) {n : ℕ} : x ^ n ≤ 1 - pow_le_pow_left' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] [MulRightMono M] {a b : M} (hab : a ≤ b) (i : ℕ) : a ^ i ≤ b ^ i - Right.pow_lt_one_of_lt 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [Monoid M] [Preorder M] [MulRightMono M] {n : ℕ} {x : M} (hn : 0 < n) (h : x < 1) : x ^ n < 1 - pow_le_pow 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] [MulRightMono M] {a b : M} (hab : a ≤ b) (ht : 1 ≤ b) {m n : ℕ} (hmn : m ≤ n) : a ^ m ≤ b ^ n - le_pow_sup 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [Monoid M] [SemilatticeSup M] [MulLeftMono M] [MulRightMono M] {a b : M} {n : ℕ} : a ^ n ⊔ b ^ n ≤ (a ⊔ b) ^ n - pow_inf_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [Monoid M] [SemilatticeInf M] [MulLeftMono M] [MulRightMono M] {a b : M} {n : ℕ} : (a ⊓ b) ^ n ≤ a ^ n ⊓ b ^ n - lt_of_pow_lt_pow_left' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [Monoid M] [LinearOrder M] [MulLeftMono M] [MulRightMono M] {a b : M} (n : ℕ) : a ^ n < b ^ n → a < b - lt_max_of_sq_lt_mul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [Monoid M] [LinearOrder M] [MulLeftMono M] [MulRightMono M] {a b c : M} (h : a ^ 2 < b * c) : a < max b c - min_lt_of_mul_lt_sq 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [Monoid M] [LinearOrder M] [MulLeftMono M] [MulRightMono M] {a b c : M} (h : a * b < c ^ 2) : min a b < c - pow_le_pow_mul_of_sq_le_mul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [Monoid M] [Preorder M] [MulRightMono M] [MulLeftMono M] {a b : M} (hab : a ^ 2 ≤ b * a) {n : ℕ} : n ≠ 0 → a ^ n ≤ b ^ (n - 1) * a - inf_div 📋 Mathlib.Algebra.Order.Group.Lattice
{α : Type u_1} [Lattice α] [Group α] [MulRightMono α] (a b c : α) : (a ⊓ b) / c = a / c ⊓ b / c - sup_div 📋 Mathlib.Algebra.Order.Group.Lattice
{α : Type u_1} [Lattice α] [Group α] [MulRightMono α] (a b c : α) : (a ⊔ b) / c = a / c ⊔ b / c - inf_mul 📋 Mathlib.Algebra.Order.Group.Lattice
{α : Type u_1} [Lattice α] [Group α] [MulRightMono α] (a b c : α) : (a ⊓ b) * c = a * c ⊓ b * c - inv_inf 📋 Mathlib.Algebra.Order.Group.Lattice
{α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a b : α) : (a ⊓ b)⁻¹ = a⁻¹ ⊔ b⁻¹ - inv_sup 📋 Mathlib.Algebra.Order.Group.Lattice
{α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a b : α) : (a ⊔ b)⁻¹ = a⁻¹ ⊓ b⁻¹ - sup_mul 📋 Mathlib.Algebra.Order.Group.Lattice
{α : Type u_1} [Lattice α] [Group α] [MulRightMono α] (a b c : α) : (a ⊔ b) * c = a * c ⊔ b * c - div_inf 📋 Mathlib.Algebra.Order.Group.Lattice
{α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a b c : α) : c / (a ⊓ b) = c / a ⊔ c / b - div_sup 📋 Mathlib.Algebra.Order.Group.Lattice
{α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a b c : α) : c / (a ⊔ b) = c / a ⊓ c / b - pow_two_semiclosed 📋 Mathlib.Algebra.Order.Group.Lattice
{α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] {a : α} (ha : 1 ≤ a ^ 2) : 1 ≤ a - mabs_mabs 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a : α) : |(|a|ₘ)|ₘ = |a|ₘ - one_le_mabs 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a : α) : 1 ≤ |a|ₘ - mabs_eq_one 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] {a : α} [MulRightMono α] : |a|ₘ = 1 ↔ a = 1 - mabs_ne_one 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] {a : α} [MulRightMono α] : |a|ₘ ≠ 1 ↔ a ≠ 1 - inv_lt_of_mabs_lt 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] {a b : α} [MulRightMono α] (h : |a|ₘ < b) : b⁻¹ < a - mabs_le_one 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] {a : α} [MulRightMono α] : |a|ₘ ≤ 1 ↔ a = 1 - max_div_min_eq_mabs 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] [MulRightMono α] (a b : α) : max a b / min a b = |b / a|ₘ - max_div_min_eq_mabs' 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] [MulRightMono α] (a b : α) : max a b / min a b = |a / b|ₘ - mabs_lt 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] {a b : α} [MulRightMono α] : |a|ₘ < b ↔ b⁻¹ < a ∧ a < b - mabs_le_mabs_of_le_one 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] {a b : α} [MulRightMono α] (ha : a ≤ 1) (hab : b ≤ a) : |a|ₘ ≤ |b|ₘ - Pi.mabs_eq_one 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Group (α i)] (f : (i : ι) → α i) [(i : ι) → LinearOrder (α i)] [∀ (i : ι), MulLeftMono (α i)] [∀ (i : ι), MulRightMono (α i)] : |f|ₘ = 1 ↔ f = 1 - mabs_div_lt_of_lt_lt 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] [MulRightMono α] {N M n m : α} (hn : 1 ≤ n) (hm : 1 ≤ m) (hnN : n < N) (hmM : m < M) : |n / m|ₘ < max N M - 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) - 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) - CanonicallyOrderedAdd.toMulRightMono 📋 Mathlib.Algebra.Order.Ring.Canonical
{R : Type u} [NonUnitalNonAssocSemiring R] [LE R] [CanonicallyOrderedAdd R] : MulRightMono R - tsub_mul 📋 Mathlib.Algebra.Order.Ring.Canonical
{R : Type u} [NonUnitalNonAssocSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Sub R] [OrderedSub R] [Std.Total fun x1 x2 => x1 ≤ x2] [AddLeftReflectLE R] [MulRightMono R] (a b c : R) : (a - b) * c = a * c - b * c - tsub_one_mul 📋 Mathlib.Algebra.Order.Ring.Canonical
{R : Type u} [NonAssocSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Sub R] [OrderedSub R] [Std.Total fun x1 x2 => x1 ≤ x2] [MulRightMono R] [AddLeftReflectLE R] (a b : R) : (a - 1) * b = a * b - b - AddLECancellable.tsub_mul 📋 Mathlib.Algebra.Order.Ring.Canonical
{R : Type u} [NonUnitalNonAssocSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Sub R] [OrderedSub R] [Std.Total fun x1 x2 => x1 ≤ x2] [MulRightMono R] {a b c : R} (h : AddLECancellable (b * c)) : (a - b) * c = a * c - b * c - leOnePart_anti 📋 Mathlib.Algebra.Order.Group.PosPart
{α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] : Antitone leOnePart - oneLePart_inf_leOnePart_eq_one 📋 Mathlib.Algebra.Order.Group.PosPart
{α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a : α) : a⁺ᵐ ⊓ a⁻ᵐ = 1 - leOnePart_mul_oneLePart 📋 Mathlib.Algebra.Order.Group.PosPart
{α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a : α) : a⁻ᵐ * a⁺ᵐ = |a|ₘ - oneLePart_mul_leOnePart 📋 Mathlib.Algebra.Order.Group.PosPart
{α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a : α) : a⁺ᵐ * a⁻ᵐ = |a|ₘ - leOnePart_eq_inv_inf_one 📋 Mathlib.Algebra.Order.Group.PosPart
{α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a : α) : a⁻ᵐ = (a ⊓ 1)⁻¹ - leOnePart_min 📋 Mathlib.Algebra.Order.Group.PosPart
{α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a b : α) : (a ⊓ b)⁻ᵐ = a⁻ᵐ ⊔ b⁻ᵐ - leOnePart_max 📋 Mathlib.Algebra.Order.Group.PosPart
{α : Type u_1} [DistribLattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a b : α) : (a ⊔ b)⁻ᵐ = a⁻ᵐ ⊓ b⁻ᵐ - leOnePart_lt 📋 Mathlib.Algebra.Order.Group.PosPart
{α : Type u_1} [LinearOrder α] [Group α] {a b : α} [MulLeftMono α] [MulRightMono α] : a⁻ᵐ < b ↔ b⁻¹ < a ∧ 1 < b - Set.instMulRightMono 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} [Mul α] : MulRightMono (Set α) - List.pow_card_le_prod 📋 Mathlib.Algebra.Order.BigOperators.Group.List
{M : Type u_3} [Monoid M] [Preorder M] [MulRightMono M] [MulLeftMono M] (l : List M) (n : M) (h : ∀ x ∈ l, n ≤ x) : n ^ l.length ≤ l.prod - List.pow_length_le_prod 📋 Mathlib.Algebra.Order.BigOperators.Group.List
{M : Type u_3} [Monoid M] [Preorder M] [MulRightMono M] [MulLeftMono M] (l : List M) (n : M) (h : ∀ x ∈ l, n ≤ x) : n ^ l.length ≤ l.prod - List.prod_le_pow_card 📋 Mathlib.Algebra.Order.BigOperators.Group.List
{M : Type u_3} [Monoid M] [Preorder M] [MulRightMono M] [MulLeftMono M] (l : List M) (n : M) (h : ∀ x ∈ l, x ≤ n) : l.prod ≤ n ^ l.length - List.prod_le_pow_length 📋 Mathlib.Algebra.Order.BigOperators.Group.List
{M : Type u_3} [Monoid M] [Preorder M] [MulRightMono M] [MulLeftMono M] (l : List M) (n : M) (h : ∀ x ∈ l, x ≤ n) : l.prod ≤ n ^ l.length - List.Forall₂.prod_le_prod' 📋 Mathlib.Algebra.Order.BigOperators.Group.List
{M : Type u_3} [Monoid M] [Preorder M] [MulRightMono M] [MulLeftMono M] {l₁ l₂ : List M} (h : List.Forall₂ (fun x1 x2 => x1 ≤ x2) l₁ l₂) : l₁.prod ≤ l₂.prod - List.prod_le_prod' 📋 Mathlib.Algebra.Order.BigOperators.Group.List
{ι : Type u_1} {M : Type u_3} [Monoid M] [Preorder M] [MulRightMono M] [MulLeftMono M] {l : List ι} {f g : ι → M} (h : ∀ i ∈ l, f i ≤ g i) : (List.map f l).prod ≤ (List.map g l).prod - List.Sublist.prod_le_prod' 📋 Mathlib.Algebra.Order.BigOperators.Group.List
{M : Type u_3} [Monoid M] [Preorder M] [MulRightMono M] [MulLeftMono M] {l₁ l₂ : List M} (h : l₁.Sublist l₂) (h₁ : ∀ a ∈ l₂, 1 ≤ a) : l₁.prod ≤ l₂.prod - List.SublistForall₂.prod_le_prod' 📋 Mathlib.Algebra.Order.BigOperators.Group.List
{M : Type u_3} [Monoid M] [Preorder M] [MulRightMono M] [MulLeftMono M] {l₁ l₂ : List M} (h : List.SublistForall₂ (fun x1 x2 => x1 ≤ x2) l₁ l₂) (h₁ : ∀ a ∈ l₂, 1 ≤ a) : l₁.prod ≤ l₂.prod - List.prod_lt_prod_of_ne_nil 📋 Mathlib.Algebra.Order.BigOperators.Group.List
{ι : Type u_1} {M : Type u_3} [Monoid M] [Preorder M] [MulLeftStrictMono M] [MulLeftMono M] [MulRightStrictMono M] [MulRightMono M] {l : List ι} (hl : l ≠ []) (f g : ι → M) (hlt : ∀ i ∈ l, f i < g i) : (List.map f l).prod < (List.map g l).prod - List.exists_lt_of_prod_lt' 📋 Mathlib.Algebra.Order.BigOperators.Group.List
{ι : Type u_1} {M : Type u_3} [Monoid M] [LinearOrder M] [MulRightMono M] [MulLeftMono M] {l : List ι} (f g : ι → M) (h : (List.map f l).prod < (List.map g l).prod) : ∃ i ∈ l, f i < g i - List.prod_lt_prod' 📋 Mathlib.Algebra.Order.BigOperators.Group.List
{ι : Type u_1} {M : Type u_3} [Monoid M] [Preorder M] [MulLeftStrictMono M] [MulLeftMono M] [MulRightStrictMono M] [MulRightMono M] {l : List ι} (f g : ι → M) (h₁ : ∀ i ∈ l, f i ≤ g i) (h₂ : ∃ i ∈ l, f i < g i) : (List.map f l).prod < (List.map g l).prod - List.max_prod_le 📋 Mathlib.Algebra.Order.BigOperators.Group.List
{α : Type u_2} {M : Type u_3} [Monoid M] (l : List α) (f g : α → M) [LinearOrder M] [MulLeftMono M] [MulRightMono M] : max (List.map f l).prod (List.map g l).prod ≤ (List.map (fun i => max (f i) (g i)) l).prod - List.prod_min_le 📋 Mathlib.Algebra.Order.BigOperators.Group.List
{α : Type u_2} {M : Type u_3} [Monoid M] [LinearOrder M] [MulLeftMono M] [MulRightMono M] (l : List α) (f g : α → M) : (List.map (fun i => min (f i) (g i)) l).prod ≤ min (List.map f l).prod (List.map g l).prod - List.exists_le_of_prod_le' 📋 Mathlib.Algebra.Order.BigOperators.Group.List
{ι : Type u_1} {M : Type u_3} [Monoid M] [LinearOrder M] [MulLeftStrictMono M] [MulLeftMono M] [MulRightStrictMono M] [MulRightMono M] {l : List ι} (hl : l ≠ []) (f g : ι → M) (h : (List.map f l).prod ≤ (List.map g l).prod) : ∃ x ∈ l, f x ≤ g x - MonoidHomClass.ext_iff_le 📋 Mathlib.Algebra.Order.Hom.Monoid
{α : Type u_2} {β : Type u_3} [Group α] [Monoid β] {F : Type u_6} [FunLike F α β] [MonoidHomClass F α β] [PartialOrder β] [MulRightMono β] [MulLeftMono β] {f g : F} : f = g ↔ ∀ (x : α), f x ≤ g x - map_inv_le_map_inv_iff_map_le_map 📋 Mathlib.Algebra.Order.Hom.Monoid
{α : Type u_2} {β : Type u_3} [Group α] [Monoid β] {F : Type u_6} [FunLike F α β] [MonoidHomClass F α β] [LE β] [MulRightMono β] [MulLeftMono β] {f g : F} {x : α} : f x⁻¹ ≤ g x⁻¹ ↔ g x ≤ f x - Ordinal.mulRightMono 📋 Mathlib.SetTheory.Ordinal.Arithmetic
: MulRightMono Ordinal.{u} - Finset.instMulRightMono 📋 Mathlib.Algebra.Group.Pointwise.Finset.Basic
{α : Type u_2} [DecidableEq α] [Mul α] : MulRightMono (Finset α) - IdemSemiring.toMulRightMono 📋 Mathlib.Algebra.Order.Kleene
{α : Type u_1} [IdemSemiring α] : MulRightMono α - SetSemiring.mulRightMono 📋 Mathlib.Data.Set.Semiring
{α : Type u_1} [Mul α] : MulRightMono (SetSemiring α) - Submodule.instMulRightMono 📋 Mathlib.Algebra.Algebra.Operations
{R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] : MulRightMono (Submodule R A) - Finset.sup'_mul 📋 Mathlib.Algebra.Order.Group.Finset
{ι : Type u_1} {G : Type u_4} [Group G] [LinearOrder G] [MulRightMono G] (s : Finset ι) (f : ι → G) (a : G) (hs : s.Nonempty) : s.sup' hs f * a = s.sup' hs fun i => f i * a - Finset.inf'_pow 📋 Mathlib.Algebra.Order.Group.Finset
{ι : Type u_1} {M : Type u_3} [LinearOrder M] [Monoid M] [MulLeftMono M] [MulRightMono M] (s : Finset ι) (f : ι → M) (n : ℕ) (hs : s.Nonempty) : s.inf' hs f ^ n = s.inf' hs fun a => f a ^ n - Finset.sup'_pow 📋 Mathlib.Algebra.Order.Group.Finset
{ι : Type u_1} {M : Type u_3} [LinearOrder M] [Monoid M] [MulLeftMono M] [MulRightMono M] (s : Finset ι) (f : ι → M) (n : ℕ) (hs : s.Nonempty) : s.sup' hs f ^ n = s.sup' hs fun a => f a ^ n - Filter.mulRightMono 📋 Mathlib.Order.Filter.Pointwise
{α : Type u_2} [Mul α] : MulRightMono (Filter α) - Set.Ici_mul_Ici_subset' 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
{α : Type u_1} [Mul α] [Preorder α] [MulLeftMono α] [MulRightMono α] (a b : α) : Set.Ici a * Set.Ici b ⊆ Set.Ici (a * b) - Set.Iic_mul_Iic_subset' 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
{α : Type u_1} [Mul α] [Preorder α] [MulLeftMono α] [MulRightMono α] (a b : α) : Set.Iic a * Set.Iic b ⊆ Set.Iic (a * b) - Set.Icc_mul_Icc_subset' 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
{α : Type u_1} [Mul α] [Preorder α] [MulLeftMono α] [MulRightMono α] (a b c d : α) : Set.Icc a b * Set.Icc c d ⊆ Set.Icc (a * c) (b * d) - Set.Ici_mul_Ici_eq 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
{α : Type u_2} [Monoid α] [Preorder α] [CanonicallyOrderedMul α] [MulRightMono α] {a b : α} : Set.Ici a * Set.Ici b = Set.Ici (a * b) - Set.Ici_pow_eq 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
{α : Type u_2} [Monoid α] [Preorder α] [CanonicallyOrderedMul α] [MulRightMono α] {a : α} (n : ℕ) : n ≠ 0 → Set.Ici a ^ n = Set.Ici (a ^ n) - Finset.Ici_mul_Ici_subset' 📋 Mathlib.Algebra.Group.Pointwise.Finset.Interval
{α : Type u_1} [Mul α] [Preorder α] [DecidableEq α] [MulLeftMono α] [MulRightMono α] [LocallyFiniteOrderTop α] (a b : α) : Finset.Ici a * Finset.Ici b ⊆ Finset.Ici (a * b) - Finset.Iic_mul_Iic_subset' 📋 Mathlib.Algebra.Group.Pointwise.Finset.Interval
{α : Type u_1} [Mul α] [Preorder α] [DecidableEq α] [MulLeftMono α] [MulRightMono α] [LocallyFiniteOrderBot α] (a b : α) : Finset.Iic a * Finset.Iic b ⊆ Finset.Iic (a * b) - Finset.Icc_mul_Icc_subset' 📋 Mathlib.Algebra.Group.Pointwise.Finset.Interval
{α : Type u_1} [Mul α] [Preorder α] [DecidableEq α] [MulLeftMono α] [MulRightMono α] [LocallyFiniteOrder α] (a b c d : α) : Finset.Icc a b * Finset.Icc c d ⊆ Finset.Icc (a * c) (b * d) - instMulPosMonoWithZeroOfMulRightMono 📋 Mathlib.Algebra.Order.GroupWithZero.WithZero
{α : Type u_1} [Mul α] [Preorder α] [MulRightMono α] : MulPosMono (WithZero α) - FractionalIdeal.instMulRightMono 📋 Mathlib.RingTheory.FractionalIdeal.Basic
{R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : MulRightMono (FractionalIdeal S P) - BddAbove.mul 📋 Mathlib.Algebra.Order.Group.Pointwise.Bounds
{M : Type u_3} [Mul M] [Preorder M] [MulLeftMono M] [MulRightMono M] {s t : Set M} (hs : BddAbove s) (ht : BddAbove t) : BddAbove (s * t)
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:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"somewhere in their lemma name.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 ?aIf 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 ?bBy 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 findtsum_lt_tsumeven though the hypothesisf i < g iis not the last.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