Loogle!
Result
Found 439 declarations mentioning MulLeftMono. Of these, only the first 200 are shown.
- MulLeftMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
(M : Type u_1) [Mul M] [LE M] : Prop - mulLeftMono_of_mulLeftStrictMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
(M : Type u_3) [Mul M] [PartialOrder M] [MulLeftStrictMono M] : MulLeftMono M - mulRightMono_of_mulLeftMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
(N : Type u_2) [CommSemigroup N] [LE N] [MulLeftMono N] : MulRightMono N - IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
(N : Type u_2) [Mul N] [IsLeftCancelMul N] [PartialOrder N] [MulLeftMono N] : MulLeftStrictMono N - mulLeftReflectLT_of_mulLeftMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
(N : Type u_2) [Mul N] [LinearOrder N] [MulLeftMono N] : MulLeftReflectLT N - Group.mulLeftReflectLE_of_mulLeftMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
{N : Type u_2} [Group N] [LE N] [MulLeftMono N] : MulLeftReflectLE N - Nat.instMulLeftMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
: MulLeftMono ℕ - mul_right_mono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a : α} [Mul α] [Preorder α] [MulLeftMono α] : Monotone fun x => a * x - MulLECancellable.of_mul_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b : α} [LE α] [Semigroup α] [MulLeftMono α] (h : MulLECancellable (a * b)) : MulLECancellable b - mul_le_mul_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {b c : α} [Mul α] [LE α] [MulLeftMono α] (bc : b ≤ c) (a : α) : a * b ≤ a * c - Antitone.const_mul' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : β → α} [MulLeftMono α] (hf : Antitone f) (a : α) : Antitone fun x => a * f x - Monotone.const_mul' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : β → α} [MulLeftMono α] (hf : Monotone f) (a : α) : Monotone fun x => a * f x - mulLeftStrictMono_iff_mulLeftMono_and_isLeftCancelMul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [Mul α] [LinearOrder α] : MulLeftStrictMono α ↔ MulLeftMono α ∧ IsLeftCancelMul α - mul_le_mul_iff_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [Mul α] [LE α] [MulLeftMono α] [MulLeftReflectLE α] (a : α) {b c : α} : a * b ≤ a * c ↔ b ≤ c - AntitoneOn.const_mul' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : β → α} {s : Set β} [MulLeftMono α] (hf : AntitoneOn f s) (a : α) : AntitoneOn (fun x => a * f x) s - MonotoneOn.const_mul' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : β → α} {s : Set β} [MulLeftMono α] (hf : MonotoneOn f s) (a : α) : MonotoneOn (fun x => a * f x) s - MulLECancellable.mul_le_mul_iff_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [LE α] [Mul α] [MulLeftMono α] (ha : MulLECancellable a) : a * b ≤ a * c ↔ b ≤ c - MulLECancellable.of_mul_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b : α} [LE α] [CommSemigroup α] [MulLeftMono α] (h : MulLECancellable (a * b)) : MulLECancellable a - le_mul_of_one_le_right' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b : α} [MulOneClass α] [LE α] [MulLeftMono α] (h : 1 ≤ b) : a ≤ a * b - mul_le_of_le_one_right' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b : α} [MulOneClass α] [LE α] [MulLeftMono α] (h : b ≤ 1) : a * b ≤ a - MulLECancellable.mul_le_mul_iff_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [LE α] [Mul α] [IsMulCommutative α] [MulLeftMono α] (ha : MulLECancellable a) : b * a ≤ c * a ↔ b ≤ c - le_mul_of_le_mul_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Mul α] [Preorder α] [MulLeftMono α] (h : a ≤ b * c) (hle : c ≤ d) : a ≤ b * d - lt_mul_of_lt_mul_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Mul α] [Preorder α] [MulLeftMono α] (h : a < b * c) (hle : c ≤ d) : a < b * d - mul_le_of_mul_le_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Mul α] [Preorder α] [MulLeftMono α] (h : a * b ≤ c) (hle : d ≤ b) : a * d ≤ c - mul_lt_of_mul_lt_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Mul α] [Preorder α] [MulLeftMono α] (h : a * b < c) (hle : d ≤ b) : a * d < 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 - 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 - StrictAnti.mul_antitone' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f g : β → α} [MulLeftMono α] [MulRightStrictMono α] (hf : StrictAnti f) (hg : Antitone g) : StrictAnti fun x => f x * g x - StrictMono.mul_monotone' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f g : β → α} [MulLeftMono α] [MulRightStrictMono α] (hf : StrictMono f) (hg : Monotone g) : StrictMono fun x => f x * g x - le_mul_iff_one_le_right' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {b : α} [MulOneClass α] [LE α] [MulLeftMono α] [MulLeftReflectLE α] (a : α) : a ≤ a * b ↔ 1 ≤ b - mul_le_iff_le_one_right' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {b : α} [MulOneClass α] [LE α] [MulLeftMono α] [MulLeftReflectLE α] (a : α) : a * b ≤ a ↔ b ≤ 1 - mulLECancellable_mul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b : α} [LE α] [CommSemigroup α] [MulLeftMono α] : MulLECancellable (a * b) ↔ MulLECancellable a ∧ MulLECancellable b - MulLECancellable.le_mul_iff_one_le_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b : α} [LE α] [MulOneClass α] [MulLeftMono α] (ha : MulLECancellable a) : a ≤ a * b ↔ 1 ≤ b - MulLECancellable.mul_le_iff_le_one_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b : α} [LE α] [MulOneClass α] [MulLeftMono α] (ha : MulLECancellable a) : a * b ≤ a ↔ b ≤ 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_lt_of_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Mul α] [Preorder α] [MulLeftMono α] [MulRightStrictMono α] (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 - 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 - Right.mul_lt_mul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Mul α] [Preorder α] [MulLeftMono α] [MulRightStrictMono α] (h₁ : a < b) (h₂ : c < d) : a * c < b * d - StrictAntiOn.mul_antitone' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f g : β → α} {s : Set β} [MulLeftMono α] [MulRightStrictMono α] (hf : StrictAntiOn f s) (hg : AntitoneOn g s) : StrictAntiOn (fun x => f x * g x) s - StrictMonoOn.mul_monotone' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f g : β → α} {s : Set β} [MulLeftMono α] [MulRightStrictMono α] (hf : StrictMonoOn f s) (hg : MonotoneOn g s) : StrictMonoOn (fun x => f x * g x) s - le_mul_of_le_of_one_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulLeftMono α] (hbc : b ≤ c) (ha : 1 ≤ a) : b ≤ c * a - le_of_le_mul_of_le_one_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulLeftMono α] (h : a ≤ b * c) (hle : c ≤ 1) : a ≤ b - le_of_mul_le_of_one_le_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulLeftMono α] (h : a * b ≤ c) (hle : 1 ≤ b) : a ≤ c - lt_mul_of_lt_of_one_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulLeftMono α] (hbc : b < c) (ha : 1 ≤ a) : b < c * a - lt_mul_of_lt_of_one_lt' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulLeftMono α] (hbc : b < c) (ha : 1 < a) : b < c * a - lt_of_lt_mul_of_le_one_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulLeftMono α] (h : a < b * c) (hle : c ≤ 1) : a < b - lt_of_mul_lt_of_one_le_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulLeftMono α] (h : a * b < c) (hle : 1 ≤ b) : a < c - mul_le_of_le_of_le_one 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulLeftMono α] (hbc : b ≤ c) (ha : a ≤ 1) : b * a ≤ c - mul_le_one' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulLeftMono α] (hbc : b ≤ c) (ha : a ≤ 1) : b * a ≤ c - mul_lt_of_lt_of_le_one 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulLeftMono α] (hbc : b < c) (ha : a ≤ 1) : b * a < c - mul_lt_of_lt_of_lt_one' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulLeftMono α] (hbc : b < c) (ha : a < 1) : b * a < c - mul_lt_one' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulLeftMono α] (hbc : b < c) (ha : a < 1) : b * a < c - mul_lt_one_of_lt_of_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulLeftMono α] (hbc : b < c) (ha : a ≤ 1) : b * a < c - one_lt_mul'' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulLeftMono α] (hbc : b < c) (ha : 1 < a) : b < c * a - one_lt_mul_of_lt_of_le' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulLeftMono α] (hbc : b < c) (ha : 1 ≤ a) : b < c * a - Left.mul_le_one 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulLeftMono α] (hbc : b ≤ c) (ha : a ≤ 1) : b * a ≤ c - Left.mul_lt_one' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulLeftMono α] (hbc : b < c) (ha : a < 1) : b * a < c - Left.mul_lt_one_of_lt_of_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulLeftMono α] (hbc : b < c) (ha : a ≤ 1) : b * a < c - Left.one_lt_mul' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulLeftMono α] (hbc : b < c) (ha : 1 < a) : b < c * a - Left.one_lt_mul_of_lt_of_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [MulOneClass α] [Preorder α] [MulLeftMono α] (hbc : b < c) (ha : 1 ≤ a) : b < c * a - MulLECancellable.le_mul_iff_one_le_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b : α} [LE α] [MulOneClass α] [IsMulCommutative α] [MulLeftMono α] (ha : MulLECancellable a) : a ≤ b * a ↔ 1 ≤ b - MulLECancellable.mul_le_iff_le_one_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b : α} [LE α] [MulOneClass α] [IsMulCommutative α] [MulLeftMono α] (ha : MulLECancellable a) : b * a ≤ a ↔ b ≤ 1 - one_lt_mul_of_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [MulOneClass α] [Preorder α] [IsBotOneClass α] [MulLeftMono α] {a : α} (ha : 1 < a) (b : α) : 1 < a * b - Left.one_lt_mul_of_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [MulOneClass α] [Preorder α] [IsBotOneClass α] [MulLeftMono α] {a : α} (ha : 1 < a) (b : α) : 1 < a * b - mul_max 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [Mul α] [LinearOrder α] [MulLeftMono α] (a b c : α) : a * max b c = max (a * b) (a * c) - mul_min 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [Mul α] [LinearOrder α] [MulLeftMono α] (a b c : α) : a * min b c = min (a * b) (a * c) - one_le_mul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b : α} [MulOneClass α] [Preorder α] [MulLeftMono α] (ha : 1 ≤ a) (hb : 1 ≤ b) : 1 ≤ a * b - Left.one_le_mul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b : α} [MulOneClass α] [Preorder α] [MulLeftMono α] (ha : 1 ≤ a) (hb : 1 ≤ b) : 1 ≤ a * b - 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_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b : α} [MulOneClass α] [PartialOrder α] [MulLeftMono α] (ha : 1 ≤ a) (hb : 1 ≤ b) (hab : a * b ≤ 1) : a = 1 - eq_one_of_one_le_mul_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b : α} [MulOneClass α] [PartialOrder α] [MulLeftMono α] (ha : a ≤ 1) (hb : b ≤ 1) (hab : 1 ≤ a * b) : a = 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 - Right.min_le_max_of_mul_le_mul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c d : α} [Mul α] [LinearOrder α] [MulLeftMono α] [MulRightStrictMono α] (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_self_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulLeftMono α] (a : α) {b : α} : a / b ≤ a ↔ 1 ≤ b - le_div_self_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulLeftMono α] (a : α) {b : α} : a ≤ a / b ↔ b ≤ 1 - Left.inv_le_self 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [Preorder α] [MulLeftMono α] {a : α} (h : 1 ≤ a) : a⁻¹ ≤ a - Left.self_le_inv 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [Preorder α] [MulLeftMono α] {a : α} (h : a ≤ 1) : a ≤ a⁻¹ - div_le_comm 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [CommGroup α] [LE α] [MulLeftMono α] {a b c : α} : a / b ≤ c ↔ a / c ≤ b - le_div_comm 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [CommGroup α] [LE α] [MulLeftMono α] {a b c : α} : a ≤ b / c ↔ c ≤ b / a - le_one_of_one_le_inv 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulLeftMono α] {a : α} : 1 ≤ a⁻¹ → a ≤ 1 - one_le_of_inv_le_one 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulLeftMono α] {a : α} : a⁻¹ ≤ 1 → 1 ≤ a - 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 - inv_le_one' 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulLeftMono α] {a : α} : a⁻¹ ≤ 1 ↔ 1 ≤ a - one_le_inv' 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulLeftMono α] {a : α} : 1 ≤ a⁻¹ ↔ a ≤ 1 - Left.inv_le_one_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulLeftMono α] {a : α} : a⁻¹ ≤ 1 ↔ 1 ≤ a - Left.one_le_inv_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulLeftMono α] {a : α} : 1 ≤ a⁻¹ ↔ a ≤ 1 - div_le_iff_le_mul' 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [CommGroup α] [LE α] [MulLeftMono α] {a b c : α} : a / b ≤ c ↔ a ≤ b * c - le_div_iff_mul_le' 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [CommGroup α] [LE α] [MulLeftMono α] {a b c : α} : b ≤ c / a ↔ a * b ≤ c - 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 α] [MulLeftMono α] {a b : α} : a⁻¹ ≤ b ↔ 1 ≤ a * b - inv_mul_le_one_iff 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulLeftMono α] {a b : α} : a⁻¹ * b ≤ 1 ↔ b ≤ a - le_inv_iff_mul_le_one_left 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulLeftMono α] {a b : α} : a ≤ b⁻¹ ↔ b * a ≤ 1 - le_inv_mul_iff_le 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulLeftMono α] {a b : α} : 1 ≤ b⁻¹ * a ↔ b ≤ a - div_le_div'' 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [CommGroup α] [Preorder α] [MulLeftMono α] {a b c d : α} (hab : a ≤ b) (hcd : c ≤ d) : a / d ≤ b / c - inv_mul_le_of_le_mul 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulLeftMono α] {a b c : α} : a ≤ b * c → b⁻¹ * a ≤ c - le_inv_mul_of_mul_le 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulLeftMono α] {a b c : α} : a * b ≤ c → b ≤ a⁻¹ * c - mul_le_of_le_inv_mul 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulLeftMono α] {a b c : α} : b ≤ a⁻¹ * c → a * b ≤ c - inv_mul_le_iff_le_mul 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulLeftMono α] {a b c : α} : b⁻¹ * a ≤ c ↔ a ≤ b * c - le_inv_mul_iff_mul_le 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LE α] [MulLeftMono α] {a b c : α} : b ≤ a⁻¹ * c ↔ a * b ≤ c - inv_le_div_iff_le_mul 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [CommGroup α] [LE α] [MulLeftMono α] {a b c : α} : b⁻¹ ≤ a / c ↔ c ≤ a * b - inv_le_div_iff_le_mul' 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [CommGroup α] [LE α] [MulLeftMono α] {a b c : α} : a⁻¹ ≤ b / c ↔ c ≤ a * b - inv_mul_le_iff_le_mul' 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [CommGroup α] [LE α] [MulLeftMono α] {a b c : α} : c⁻¹ * a ≤ b ↔ a ≤ b * c - mul_inv_le_iff_le_mul' 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [CommGroup α] [LE α] [MulLeftMono α] {a b c : α} : a * b⁻¹ ≤ c ↔ a ≤ b * c - div_le_div_flip 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u_1} [CommGroup α] [LinearOrder α] [MulLeftMono α] {a b : α} : a / b ≤ b / a ↔ a ≤ b - div_le_div_iff' 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [CommGroup α] [LE α] [MulLeftMono α] {a b c d : α} : a / b ≤ c / d ↔ a * d ≤ c * b - le_of_forall_one_lt_lt_mul 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LinearOrder α] [MulLeftMono α] {a b : α} (h : ∀ (ε : α), 1 < ε → a < b * ε) : a ≤ b - le_iff_forall_one_lt_lt_mul 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [Group α] [LinearOrder α] [MulLeftMono α] {a b : α} : a ≤ b ↔ ∀ (ε : α), 1 < ε → a < b * ε - lt_or_lt_of_div_lt_div 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [CommGroup α] [LinearOrder α] [MulLeftMono α] {a b c d : α} : a / d < b / c → a < b ∨ c < d - 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 - mul_inv_le_mul_inv_iff' 📋 Mathlib.Algebra.Order.Group.Unbundled.Basic
{α : Type u} [CommGroup α] [LE α] [MulLeftMono α] {a b c d : α} : a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b - MulLeftMono.toPosMulMono 📋 Mathlib.Algebra.Order.GroupWithZero.Defs
{α : Type u_1} [Mul α] [Zero α] [Preorder α] [MulLeftMono α] : PosMulMono α - le_iff_exists_one_le_mul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
{α : Type u} [MulOneClass α] [Preorder α] [ExistsMulOfLE α] {a b : α} [MulLeftMono α] [MulLeftReflectLE α] : a ≤ b ↔ ∃ c, 1 ≤ c ∧ a * c = b - max_mul_mul_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
{α : Type u_1} [LinearOrder α] [Mul α] [MulLeftMono α] (a b c : α) : max (a * b) (a * c) = a * max b c - min_mul_mul_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
{α : Type u_1} [LinearOrder α] [Mul α] [MulLeftMono α] (a b c : α) : min (a * b) (a * c) = a * min b c - min_le_mul_of_one_le_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
{α : Type u_1} [LinearOrder α] [MulOneClass α] [MulLeftMono α] {a b : α} (hb : 1 ≤ b) : min a b ≤ a * b - le_or_lt_of_mul_le_mul 📋 Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
{α : Type u_1} [LinearOrder α] [Mul α] [MulLeftMono α] [MulRightStrictMono α] {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.toMulLeftMono 📋 Mathlib.Algebra.Order.Monoid.Defs
{α : Type u_1} [CommMonoid α] [Preorder α] [IsOrderedMonoid α] : MulLeftMono α - OrderIso.mulLeft 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [Group α] [LE α] [MulLeftMono α] (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.mulLeft_toEquiv 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [Group α] [LE α] [MulLeftMono α] (a : α) : (OrderIso.mulLeft a).toEquiv = Equiv.mulLeft a - OrderIso.mulLeft_symm 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [Group α] [LE α] [MulLeftMono α] (a : α) : (OrderIso.mulLeft a).symm = OrderIso.mulLeft 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.mulLeft_apply 📋 Mathlib.Algebra.Order.Group.OrderIso
{α : Type u} [Group α] [LE α] [MulLeftMono α] (a x : α) : (OrderIso.mulLeft a) x = a * x - 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.mulLeftMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
{α : Type u} [LE α] [Mul α] [c : MulLeftMono α] : MulLeftMono αᵒᵈ - 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 - pow_right_monotone 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] {a : M} (ha : 1 ≤ a) : Monotone fun n => 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 - le_self_pow 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] {a : M} {n : ℕ} (ha : 1 ≤ a) (hn : n ≠ 0) : a ≤ a ^ n - one_le_pow_of_one_le' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] {a : M} (ha : 1 ≤ a) (n : ℕ) : 1 ≤ a ^ n - pow_le_one' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] {a : M} (ha : a ≤ 1) (n : ℕ) : a ^ n ≤ 1 - Left.one_le_pow_of_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] {a : M} (ha : 1 ≤ a) (n : ℕ) : 1 ≤ a ^ n - Left.pow_le_one_of_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] {a : M} (ha : a ≤ 1) (n : ℕ) : a ^ 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 - one_lt_pow' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] {a : M} (ha : 1 < a) {k : ℕ} (hk : k ≠ 0) : 1 < a ^ k - pow_le_pow_right' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] {a : M} {n m : ℕ} (ha : 1 ≤ a) (h : n ≤ m) : a ^ n ≤ a ^ m - pow_le_pow_right_of_le_one' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] {a : M} {n m : ℕ} (ha : a ≤ 1) (h : n ≤ m) : a ^ m ≤ a ^ n - pow_lt_one' 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] {a : M} {n : ℕ} (h : a < 1) (hn : n ≠ 0) : a ^ n < 1 - Left.pow_lt_one_of_lt 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] {a : M} {n : ℕ} (h : a < 1) (hn : n ≠ 0) : a ^ n < 1 - one_le_zpow 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{G : Type u_2} [DivInvMonoid G] [Preorder G] [MulLeftMono G] {x : G} (H : 1 ≤ x) {n : ℤ} (hn : 0 ≤ n) : 1 ≤ x ^ n - one_lt_zpow 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{G : Type u_2} [DivInvMonoid G] [Preorder G] [MulLeftMono G] {x : G} (hx : 1 < x) {n : ℤ} (hn : 0 < n) : 1 < x ^ n - 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 - one_le_pow_iff 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [Monoid M] [LinearOrder M] [MulLeftMono M] {x : M} {n : ℕ} (hn : n ≠ 0) : 1 ≤ x ^ n ↔ 1 ≤ x - one_lt_pow_iff 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [Monoid M] [LinearOrder M] [MulLeftMono M] {x : M} {n : ℕ} (hn : n ≠ 0) : 1 < x ^ n ↔ 1 < x - pow_le_one_iff 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [Monoid M] [LinearOrder M] [MulLeftMono M] {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n ≤ 1 ↔ x ≤ 1 - pow_lt_one_iff 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Pow
{M : Type u_3} [Monoid M] [LinearOrder M] [MulLeftMono M] {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n < 1 ↔ x < 1 - 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 - CommGroup.toDistribLattice 📋 Mathlib.Algebra.Order.Group.Lattice
(α : Type u_2) [Lattice α] [CommGroup α] [MulLeftMono α] : DistribLattice α - inf_mul_sup 📋 Mathlib.Algebra.Order.Group.Lattice
{α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a b : α) : (a ⊓ b) * (a ⊔ b) = a * b - 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⁻¹ - mul_inf 📋 Mathlib.Algebra.Order.Group.Lattice
{α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] (a b c : α) : c * (a ⊓ b) = c * a ⊓ c * b - mul_sup 📋 Mathlib.Algebra.Order.Group.Lattice
{α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] (a b c : α) : c * (a ⊔ b) = c * a ⊔ c * b - 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_one 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] : |1|ₘ = 1 - mabs_of_one_le 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Lattice α] [Group α] {a : α} [MulLeftMono α] (h : 1 ≤ a) : |a|ₘ = a - mabs_of_one_lt 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Lattice α] [Group α] {a : α} [MulLeftMono α] (h : 1 < a) : |a|ₘ = a - mabs_mabs 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a : α) : |(|a|ₘ)|ₘ = |a|ₘ - inv_mabs_le 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] (a : α) : |a|ₘ⁻¹ ≤ a - mabs_of_le_one 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Lattice α] [Group α] {a : α} [MulLeftMono α] (h : a ≤ 1) : |a|ₘ = a⁻¹ - mabs_of_lt_one 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Lattice α] [Group α] {a : α} [MulLeftMono α] (h : a < 1) : |a|ₘ = a⁻¹ - inv_mabs_le_inv 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] (a : α) : |a|ₘ⁻¹ ≤ a⁻¹ - one_le_mabs 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a : α) : 1 ≤ |a|ₘ - sup_div_inf_eq_mabs_div 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a b : α) : (a ⊔ b) / (a ⊓ b) = |b / a|ₘ - one_le_mul_mabs 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] (a : α) : 1 ≤ a * |a|ₘ - one_lt_mabs 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] {a : α} : 1 < |a|ₘ ↔ a ≠ 1 - mabs_le_mabs_of_one_le 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Lattice α] [Group α] {a b : α} [MulLeftMono α] (ha : 1 ≤ a) (hab : a ≤ b) : |a|ₘ ≤ |b|ₘ - mabs_mabs_div_mabs_le 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a b : α) : ||a|ₘ / |b|ₘ|ₘ ≤ |a / b|ₘ - one_lt_mabs_of_lt_one 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] {a : α} (h : a < 1) : 1 < |a|ₘ - one_lt_mabs_pos_of_one_lt 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] {a : α} (h : 1 < 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_inf_div_inf_le_mabs 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a b c : α) : |(a ⊓ c) / (b ⊓ c)|ₘ ≤ |a / b|ₘ - mabs_ne_one 📋 Mathlib.Algebra.Order.Group.Unbundled.Abs
{α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] {a : α} [MulRightMono α] : |a|ₘ ≠ 1 ↔ a ≠ 1
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 ce5dd8c