Loogle!
Result
Found 136 declarations mentioning AddLeftReflectLE.
- AddLeftReflectLE 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
(M : Type u_1) [Add M] [LE M] : Prop - addRightReflectLE_of_addLeftReflectLE 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
(N : Type u_2) [AddCommSemigroup N] [LE N] [AddLeftReflectLE N] : AddRightReflectLE N - IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
(N : Type u_2) [Add N] [IsLeftCancelAdd N] [PartialOrder N] [AddLeftReflectLT N] : AddLeftReflectLE N - addLeftStrictMono_of_addLeftReflectLE 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
(N : Type u_2) [Add N] [LinearOrder N] [AddLeftReflectLE N] : AddLeftStrictMono N - AddGroup.addLeftReflectLE_of_addLeftMono 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
{N : Type u_2} [AddGroup N] [LE N] [AddLeftMono N] : AddLeftReflectLE N - AddLeftReflectLE.le_of_add_le_add_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
{M : Type u_1} {inst✝ : Add M} {inst✝¹ : LE M} [self : AddLeftReflectLE M] {a b₁ b₂ : M} : a + b₁ ≤ a + b₂ → b₁ ≤ b₂ - AddLeftReflectLE.mk 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
{M : Type u_1} [Add M] [LE M] (le_of_add_le_add_left : ∀ {a b₁ b₂ : M}, a + b₁ ≤ a + b₂ → b₁ ≤ b₂) : AddLeftReflectLE M - Contravariant.AddLECancellable 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a : α} [Add α] [LE α] [AddLeftReflectLE α] : AddLECancellable a - instIsLeftCancelAddOfAddLeftReflectLE 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [Add α] [PartialOrder α] [AddLeftReflectLE α] : IsLeftCancelAdd α - Contravariant.toAddLeftCancelSemigroup 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [AddSemigroup α] [PartialOrder α] [AddLeftReflectLE α] : AddLeftCancelSemigroup α - le_of_add_le_add_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b c : α} [Add α] [LE α] [AddLeftReflectLE α] (bc : a + b ≤ a + c) : b ≤ c - add_le_add_iff_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} [Add α] [LE α] [AddLeftMono α] [AddLeftReflectLE α] (a : α) {b c : α} : a + b ≤ a + c ↔ b ≤ c - nonneg_of_le_add_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b : α} [AddZeroClass α] [LE α] [AddLeftReflectLE α] (h : a ≤ a + b) : 0 ≤ b - nonpos_of_add_le_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {a b : α} [AddZeroClass α] [LE α] [AddLeftReflectLE α] (h : a + b ≤ a) : b ≤ 0 - add_le_iff_nonpos_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {b : α} [AddZeroClass α] [LE α] [AddLeftMono α] [AddLeftReflectLE α] (a : α) : a + b ≤ a ↔ b ≤ 0 - le_add_iff_nonneg_right 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Basic
{α : Type u_1} {b : α} [AddZeroClass α] [LE α] [AddLeftMono α] [AddLeftReflectLE α] (a : α) : a ≤ a + b ↔ 0 ≤ b - le_add_tsub' 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b : α} [AddLeftReflectLE α] : a ≤ a + b - b - le_add_tsub_swap 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b : α} [AddLeftReflectLE α] : a ≤ b + a - b - add_tsub_cancel_left 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [AddLeftReflectLE α] (a b : α) : a + b - a = b - add_tsub_cancel_right 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [AddLeftReflectLE α] (a b : α) : a + b - b = a - eq_tsub_of_add_eq 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : a + c = b) : a = b - c - tsub_eq_of_eq_add 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : a = c + b) : a - b = c - tsub_eq_of_eq_add_rev 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : a = b + c) : a - b = c - le_tsub_of_add_le_left 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : a + b ≤ c) : b ≤ c - a - le_tsub_of_add_le_right 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : a + b ≤ c) : a ≤ c - b - lt_add_of_tsub_lt_left 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : a - b < c) : a < b + c - lt_add_of_tsub_lt_right 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : a - c < b) : a < b + c - lt_tsub_of_add_lt_left 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] : a + c < b → c < b - a - lt_tsub_of_add_lt_right 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] : a + c < b → a < b - c - tsub_eq_tsub_of_add_eq_add 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c d : α} [AddLeftReflectLE α] (h : a + d = c + b) : a - b = c - d - add_tsub_add_eq_tsub_left 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [AddLeftMono α] [AddLeftReflectLE α] (a b c : α) : a + b - (a + c) = b - c - add_tsub_add_eq_tsub_right 📋 Mathlib.Algebra.Order.Sub.Defs
{α : Type u_1} [PartialOrder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [AddLeftMono α] [AddLeftReflectLE α] (a c b : α) : a + c - (b + c) = a - b - exists_nonneg_add_of_le 📋 Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
{α : Type u} [AddZeroClass α] [Preorder α] [ExistsAddOfLE α] {a b : α} [AddLeftReflectLE α] (h : a ≤ b) : ∃ c, 0 ≤ c ∧ a + c = b - le_iff_exists_nonneg_add 📋 Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
{α : Type u} [AddZeroClass α] [Preorder α] [ExistsAddOfLE α] {a b : α} [AddLeftMono α] [AddLeftReflectLE α] : a ≤ b ↔ ∃ c, 0 ≤ c ∧ a + c = b - mul_add_mul_le_mul_add_mul 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [PartialOrder R] {a b c d : R} [ExistsAddOfLE R] [MulPosMono R] [AddLeftMono R] [AddLeftReflectLE R] (hab : a ≤ b) (hcd : c ≤ d) : a * d + b * c ≤ a * c + b * d - mul_add_mul_le_mul_add_mul' 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [PartialOrder R] {a b c d : R} [ExistsAddOfLE R] [MulPosMono R] [AddLeftMono R] [AddLeftReflectLE R] (hba : b ≤ a) (hdc : d ≤ c) : a * d + b * c ≤ a * c + b * d - four_mul_le_pow_two_add 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [CommSemiring R] [LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddLeftReflectLE R] [AddLeftMono R] (a b : R) : 4 * a * b ≤ (a + b) ^ 2 - four_mul_le_sq_add 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [CommSemiring R] [LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddLeftReflectLE R] [AddLeftMono R] (a b : R) : 4 * a * b ≤ (a + b) ^ 2 - two_mul_le_add_pow_two 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [CommSemiring R] [LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddLeftReflectLE R] [AddLeftMono R] (a b : R) : 2 * a * b ≤ a ^ 2 + b ^ 2 - two_mul_le_add_sq 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [CommSemiring R] [LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddLeftReflectLE R] [AddLeftMono R] (a b : R) : 2 * a * b ≤ a ^ 2 + b ^ 2 - mul_nonneg_of_three 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftMono R] [AddLeftReflectLE R] (a b c : R) : 0 ≤ a * b ∨ 0 ≤ b * c ∨ 0 ≤ c * a - mul_nonneg_iff_pos_imp_nonneg 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [LinearOrder R] {a b : R} [ExistsAddOfLE R] [PosMulStrictMono R] [MulPosStrictMono R] [AddLeftMono R] [AddLeftReflectLE R] : 0 ≤ a * b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a) - mul_nonneg_iff 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Semiring R] [LinearOrder R] {a b : R} [ExistsAddOfLE R] [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftReflectLE R] [AddLeftMono R] : 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 - mul_nonneg_iff_neg_imp_nonpos 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Ring R] [LinearOrder R] {a b : R} [PosMulStrictMono R] [MulPosStrictMono R] [AddLeftMono R] [AddLeftReflectLE R] : 0 ≤ a * b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0) - mul_nonpos_iff_neg_imp_nonneg 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Ring R] [LinearOrder R] {a b : R} [PosMulStrictMono R] [MulPosStrictMono R] [AddLeftMono R] [AddLeftReflectLE R] : a * b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0) - mul_nonpos_iff_pos_imp_nonpos 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Ring R] [LinearOrder R] {a b : R} [PosMulStrictMono R] [MulPosStrictMono R] [AddLeftMono R] [AddLeftReflectLE R] : a * b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a) - mul_nonpos_iff 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [Ring R] [LinearOrder R] {a b : R} [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftReflectLE R] [AddLeftMono R] : a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b - two_mul_le_add_of_sq_eq_mul 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [CommSemiring R] [LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftReflectLE R] [AddLeftMono R] {a b r : R} (ha : 0 ≤ a) (hb : 0 ≤ b) (ht : r ^ 2 = a * b) : 2 * r ≤ a + b - two_mul_le_add_of_sq_le_mul 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
{R : Type u} [CommSemiring R] [LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftReflectLE R] [AddLeftMono R] {a b r : R} (ha : 0 ≤ a) (hb : 0 ≤ b) (ht : r ^ 2 ≤ a * b) : 2 * r ≤ a + b - IsOrderedCancelAddMonoid.toAddLeftReflectLE 📋 Mathlib.Algebra.Order.Monoid.Defs
{α : Type u_2} [AddCommMonoid α] [Preorder α] [IsOrderedCancelAddMonoid α] : AddLeftReflectLE α - OrderedCommGroup.le_of_add_le_add_left 📋 Mathlib.Algebra.Order.Group.Defs
{α : Type u_1} {a b c : α} [Add α] [LE α] [AddLeftReflectLE α] (bc : a + b ≤ a + c) : b ≤ c - OrderDual.addLeftReflectLE 📋 Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
{α : Type u} [LE α] [Add α] [AddLeftReflectLE α] : AddLeftReflectLE αᵒᵈ - WithBot.addLECancellable_coe 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
{α : Type u} [Add α] [LE α] [AddLeftReflectLE α] (a : α) : AddLECancellable ↑a - WithTop.addLECancellable_coe 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
{α : Type u} [Add α] [LE α] [AddLeftReflectLE α] (a : α) : AddLECancellable ↑a - WithBot.addLECancellable_of_ne_bot 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
{α : Type u} [Add α] {x : WithBot α} [LE α] [AddLeftReflectLE α] (hx : x ≠ ⊥) : AddLECancellable x - WithTop.addLECancellable_of_ne_top 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
{α : Type u} [Add α] {x : WithTop α} [LE α] [AddLeftReflectLE α] (hx : x ≠ ⊤) : AddLECancellable x - WithBot.addLECancellable_iff_ne_bot 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
{α : Type u} [Add α] {x : WithBot α} [Nonempty α] [Preorder α] [AddLeftReflectLE α] : AddLECancellable x ↔ x ≠ ⊥ - WithTop.addLECancellable_iff_ne_top 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
{α : Type u} [Add α] {x : WithTop α} [Nonempty α] [Preorder α] [AddLeftReflectLE α] : AddLECancellable x ↔ x ≠ ⊤ - WithBot.addLECancellable_of_lt_bot 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
{α : Type u} [Add α] {x : WithBot α} [Preorder α] [AddLeftReflectLE α] (hx : x < ⊥) : AddLECancellable x - WithTop.addLECancellable_of_lt_top 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
{α : Type u} [Add α] {x : WithTop α} [Preorder α] [AddLeftReflectLE α] (hx : x < ⊤) : AddLECancellable x - WithBot.le_of_add_le_add_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
{α : Type u} [Add α] {x y z : WithBot α} [LE α] [AddLeftReflectLE α] (hx : x ≠ ⊥) : x + y ≤ x + z → y ≤ z - WithTop.le_of_add_le_add_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
{α : Type u} [Add α] {x y z : WithTop α} [LE α] [AddLeftReflectLE α] (hx : x ≠ ⊤) : x + y ≤ x + z → y ≤ z - WithBot.add_le_add_iff_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
{α : Type u} [Add α] {x y z : WithBot α} [LE α] [AddLeftMono α] [AddLeftReflectLE α] (hx : x ≠ ⊥) : x + y ≤ x + z ↔ y ≤ z - WithTop.add_le_add_iff_left 📋 Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
{α : Type u} [Add α] {x y z : WithTop α} [LE α] [AddLeftMono α] [AddLeftReflectLE α] (hx : x ≠ ⊤) : x + y ≤ x + z ↔ y ≤ z - tsub_tsub_cancel_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b : α} [AddLeftReflectLE α] (h : a ≤ b) : b - (b - a) = a - eq_tsub_iff_add_eq_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : c ≤ b) : a = b - c ↔ a + c = b - tsub_eq_iff_eq_add_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : b ≤ a) : a - b = c ↔ a = c + b - tsub_inj_right 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h₁ : b ≤ a) (h₂ : c ≤ a) (h₃ : a - b = a - c) : b = c - tsub_lt_tsub_left_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] : b ≤ a → c < b → a - b < a - c - tsub_lt_tsub_right_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : c ≤ a) (h2 : a < b) : a - c < b - c - tsub_tsub_tsub_cancel_left 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : b ≤ a) : a - c - (a - b) = b - c - le_tsub_iff_left 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : a ≤ c) : b ≤ c - a ↔ a + b ≤ c - le_tsub_iff_right 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : a ≤ c) : b ≤ c - a ↔ b + a ≤ c - lt_tsub_iff_left_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : c ≤ b) : a < b - c ↔ c + a < b - lt_tsub_iff_right_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : c ≤ b) : a < b - c ↔ a + c < b - tsub_lt_iff_left 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (hbc : b ≤ a) : a - b < c ↔ a < b + c - tsub_lt_iff_right 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (hbc : b ≤ a) : a - b < c ↔ a < c + b - tsub_tsub_eq_add_tsub_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : c ≤ b) : a - (b - c) = a + c - b - add_tsub_assoc_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {b c : α} [AddLeftReflectLE α] (h : c ≤ b) (a : α) : a + b - c = a + (b - c) - add_tsub_tsub_cancel 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : c ≤ a) : a + b - (a - c) = b + c - le_tsub_iff_le_tsub 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h₁ : a ≤ b) (h₂ : c ≤ b) : a ≤ b - c ↔ c ≤ b - a - tsub_add_eq_add_tsub 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : b ≤ a) : a - b + c = a + c - b - tsub_lt_iff_tsub_lt 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h₁ : b ≤ a) (h₂ : c ≤ a) : a - b < c ↔ a - c < b - lt_of_tsub_lt_tsub_left_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] [AddLeftReflectLT α] (hca : c ≤ a) (h : a - b < a - c) : c < b - add_add_tsub_cancel 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (hcb : c ≤ b) : a + c + (b - c) = a + b - tsub_tsub_assoc 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h₁ : b ≤ a) (h₂ : c ≤ b) : a - (b - c) = a - b + c - tsub_lt_tsub_iff_left_of_le_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] [AddLeftReflectLT α] (h₁ : b ≤ a) (h₂ : c ≤ a) : a - b < a - c ↔ c < b - tsub_add_tsub_comm 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
{α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c d : α} [AddLeftReflectLE α] (hba : b ≤ a) (hdc : d ≤ c) : a - b + (c - d) = a + c - (b + d) - CanonicallyOrderedAddCommMonoid.toAddCancelCommMonoid 📋 Mathlib.Algebra.Order.Sub.Basic
(α : Type u_1) [AddCommMonoid α] [PartialOrder α] [Sub α] [OrderedSub α] [AddLeftReflectLE α] : AddCancelCommMonoid α - tsub_right_inj 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (hba : b ≤ a) (hca : c ≤ a) : a - b = a - c ↔ b = c - tsub_le_tsub_iff_left 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : c ≤ a) : a - b ≤ a - c ↔ c ≤ b - tsub_tsub_eq_min 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] [AddLeftReflectLE α] (a b : α) : a - (a - b) = min a b - Even.tsub 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] [AddLeftReflectLE α] {m n : α} (hm : Even m) (hn : Even n) : Even (m - n) - tsub_lt_tsub_iff_left_of_le 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : b ≤ a) : a - b < a - c ↔ c < b - tsub_lt_tsub_iff_right 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : c ≤ a) : a - c < b - c ↔ a < b - tsub_lt_self 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b : α} [AddLeftReflectLE α] : 0 < a → 0 < b → a - b < a - tsub_lt_self_iff 📋 Mathlib.Algebra.Order.Sub.Basic
{α : Type u_1} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {a b : α} [AddLeftReflectLE α] : a - b < a ↔ 0 < a ∧ 0 < b - Nat.cast_tsub 📋 Mathlib.Data.Nat.Cast.Order.Ring
{α : Type u_2} [CommSemiring α] [PartialOrder α] [IsOrderedRing α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] [AddLeftReflectLE α] (m n : ℕ) : ↑(m - n) = ↑m - ↑n - mul_tsub 📋 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] (a b c : R) : a * (b - c) = a * b - a * c - mul_tsub_one 📋 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] [AddLeftReflectLE R] (a b : R) : a * (b - 1) = a * b - a - 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 - mul_self_tsub_mul_self 📋 Mathlib.Algebra.Order.Ring.Canonical
{R : Type u} [CommSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Sub R] [OrderedSub R] [Std.Total fun x1 x2 => x1 ≤ x2] [AddLeftReflectLE R] (a b : R) : a * a - b * b = (a + b) * (a - b) - sq_tsub_sq 📋 Mathlib.Algebra.Order.Ring.Canonical
{R : Type u} [CommSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Sub R] [OrderedSub R] [Std.Total fun x1 x2 => x1 ≤ x2] [AddLeftReflectLE R] (a b : R) : a ^ 2 - b ^ 2 = (a + b) * (a - b) - mul_self_tsub_one 📋 Mathlib.Algebra.Order.Ring.Canonical
{R : Type u} [CommSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Sub R] [OrderedSub R] [Std.Total fun x1 x2 => x1 ≤ x2] [AddLeftReflectLE R] (a : R) : a * a - 1 = (a + 1) * (a - 1) - Positive.addLeftReflectLE 📋 Mathlib.Algebra.Order.Positive.Ring
{M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddLeftReflectLE M] : AddLeftReflectLE { x // 0 < x } - instAddLeftReflectLEPNat 📋 Mathlib.Data.PNat.Basic
: AddLeftReflectLE ℕ+ - Multiset.instAddLeftReflectLE 📋 Mathlib.Algebra.Order.Group.Multiset
{α : Type u_1} : AddLeftReflectLE (Multiset α) - Multiset.sum_map_tsub 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
{ι : Type u_2} {M : Type u_5} [AddCommMonoid M] [PartialOrder M] [ExistsAddOfLE M] [AddLeftMono M] [AddLeftReflectLE M] [Sub M] [OrderedSub M] (l : Multiset ι) {f g : ι → M} (hfg : ∀ x ∈ l, g x ≤ f x) : (Multiset.map (fun x => f x - g x) l).sum = (Multiset.map f l).sum - (Multiset.map g l).sum - Finset.sum_range_tsub 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] [PartialOrder M] [Sub M] [OrderedSub M] [AddLeftMono M] [AddLeftReflectLE M] [ExistsAddOfLE M] {f : ℕ → M} (h : Monotone f) (n : ℕ) : ∑ i ∈ Finset.range n, (f (i + 1) - f i) = f n - f 0 - Finset.sum_tsub_distrib 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [PartialOrder M] [Sub M] [OrderedSub M] [AddLeftMono M] [AddLeftReflectLE M] [ExistsAddOfLE M] (s : Finset ι) {f g : ι → M} (hfg : ∀ x ∈ s, g x ≤ f x) : ∑ x ∈ s, (f x - g x) = ∑ x ∈ s, f x - ∑ x ∈ s, g x - Finset.HasAntidiagonal.filter_fst_eq_antidiagonal 📋 Mathlib.Algebra.Order.Antidiag.Prod
{A : Type u_1} [AddCommMonoid A] [PartialOrder A] [CanonicallyOrderedAdd A] [Sub A] [OrderedSub A] [AddLeftReflectLE A] [Finset.HasAntidiagonal A] (n m : A) [DecidablePred fun x => x = m] [Decidable (m ≤ n)] : {x ∈ Finset.HasAntidiagonal.antidiagonal n | x.1 = m} = if m ≤ n then {(m, n - m)} else ∅ - Finset.HasAntidiagonal.filter_snd_eq_antidiagonal 📋 Mathlib.Algebra.Order.Antidiag.Prod
{A : Type u_1} [AddCommMonoid A] [PartialOrder A] [CanonicallyOrderedAdd A] [Sub A] [OrderedSub A] [AddLeftReflectLE A] [Finset.HasAntidiagonal A] (n m : A) [DecidablePred fun x => x = m] [Decidable (m ≤ n)] : {x ∈ Finset.HasAntidiagonal.antidiagonal n | x.2 = m} = if m ≤ n then {(n - m, m)} else ∅ - Ordinal.instAddLeftReflectLE 📋 Mathlib.SetTheory.Ordinal.Arithmetic
: AddLeftReflectLE Ordinal.{u} - Finset.add_sup'' 📋 Mathlib.Algebra.Order.Group.Finset
{ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [LinearOrder M] [CanonicallyOrderedAdd M] [Sub M] [AddLeftReflectLE M] [OrderedSub M] {s : Finset ι} (hs : s.Nonempty) (f : ι → M) (a : M) : a + s.sup' hs f = s.sup' hs fun i => a + f i - Finset.sup'_add' 📋 Mathlib.Algebra.Order.Group.Finset
{ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [LinearOrder M] [CanonicallyOrderedAdd M] [Sub M] [AddLeftReflectLE M] [OrderedSub M] (s : Finset ι) (f : ι → M) (a : M) (hs : s.Nonempty) : s.sup' hs f + a = s.sup' hs fun i => f i + a - Finset.add_sup 📋 Mathlib.Algebra.Order.Group.Finset
{ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [LinearOrder M] [CanonicallyOrderedAdd M] [Sub M] [AddLeftReflectLE M] [OrderedSub M] {s : Finset ι} [OrderBot M] (hs : s.Nonempty) (f : ι → M) (a : M) : a + s.sup f = s.sup fun i => a + f i - Finset.sup_add 📋 Mathlib.Algebra.Order.Group.Finset
{ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [LinearOrder M] [CanonicallyOrderedAdd M] [Sub M] [AddLeftReflectLE M] [OrderedSub M] {s : Finset ι} [OrderBot M] (hs : s.Nonempty) (f : ι → M) (a : M) : s.sup f + a = s.sup fun i => f i + a - Finset.sup_add_sup 📋 Mathlib.Algebra.Order.Group.Finset
{ι : Type u_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] [LinearOrder M] [CanonicallyOrderedAdd M] [Sub M] [AddLeftReflectLE M] [OrderedSub M] {s : Finset ι} {t : Finset κ} [OrderBot M] (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → M) (g : κ → M) : s.sup f + t.sup g = (s ×ˢ t).sup fun ij => f ij.1 + g ij.2 - Finsupp.addLeftReflectLE 📋 Mathlib.Data.Finsupp.Order
{ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [Preorder α] [AddLeftReflectLE α] : AddLeftReflectLE (ι →₀ α) - geom_sum_mul_of_le_one 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [CommSemiring R] [PartialOrder R] [AddLeftReflectLE R] [AddLeftMono R] [ExistsAddOfLE R] [Sub R] [OrderedSub R] {x : R} (hx : x ≤ 1) (n : ℕ) : (∑ i ∈ Finset.range n, x ^ i) * (1 - x) = 1 - x ^ n - geom_sum_mul_of_one_le 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [CommSemiring R] [PartialOrder R] [AddLeftReflectLE R] [AddLeftMono R] [ExistsAddOfLE R] [Sub R] [OrderedSub R] {x : R} (hx : 1 ≤ x) (n : ℕ) : (∑ i ∈ Finset.range n, x ^ i) * (x - 1) = x ^ n - 1 - geom_sum₂_mul_of_ge 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [CommSemiring R] [PartialOrder R] [AddLeftReflectLE R] [AddLeftMono R] [ExistsAddOfLE R] [Sub R] [OrderedSub R] {x y : R} (hxy : y ≤ x) (n : ℕ) : (∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n - geom_sum₂_mul_of_le 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [CommSemiring R] [PartialOrder R] [AddLeftReflectLE R] [AddLeftMono R] [ExistsAddOfLE R] [Sub R] [OrderedSub R] {x y : R} (hxy : x ≤ y) (n : ℕ) : (∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)) * (y - x) = y ^ n - x ^ n - DFinsupp.instAddLeftReflectLE 📋 Mathlib.Data.DFinsupp.Order
{ι : Type u_1} {α : ι → Type u_2} [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), AddLeftReflectLE (α i)] : AddLeftReflectLE (Π₀ (i : ι), α i) - Set.vadd_Icc 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
{α : Type u_1} [AddCommMonoid α] [LinearOrder α] [IsOrderedAddMonoid α] [AddLeftReflectLE α] [ExistsAddOfLE α] (a b c : α) : a +ᵥ Set.Icc b c = Set.Icc (a + b) (a + c) - Set.Icc_add_Icc 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
{α : Type u_1} [AddCommMonoid α] [LinearOrder α] [IsOrderedAddMonoid α] [AddLeftReflectLE α] [ExistsAddOfLE α] {a b c d : α} (hab : a ≤ b) (hcd : c ≤ d) : Set.Icc a b + Set.Icc c d = Set.Icc (a + c) (b + d) - DirectSum.coe_mul_of_apply_of_le 📋 Mathlib.Algebra.DirectSum.Internal
{ι : Type u_1} {σ : Type u_2} {R : Type u_4} [DecidableEq ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike.GradedMonoid A] [Sub ι] [OrderedSub ι] [AddLeftReflectLE ι] (r : DirectSum ι fun i => ↥(A i)) {i : ι} (r' : ↥(A i)) (n : ι) (h : i ≤ n) : ↑((r * (DirectSum.of (fun i => ↥(A i)) i) r') n) = ↑(r (n - i)) * ↑r' - DirectSum.coe_of_mul_apply_of_le 📋 Mathlib.Algebra.DirectSum.Internal
{ι : Type u_1} {σ : Type u_2} {R : Type u_4} [DecidableEq ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike.GradedMonoid A] [Sub ι] [OrderedSub ι] [AddLeftReflectLE ι] {i : ι} (r : ↥(A i)) (r' : DirectSum ι fun i => ↥(A i)) (n : ι) (h : i ≤ n) : ↑(((DirectSum.of (fun i => ↥(A i)) i) r * r') n) = ↑r * ↑(r' (n - i)) - DirectSum.coe_mul_of_apply 📋 Mathlib.Algebra.DirectSum.Internal
{ι : Type u_1} {σ : Type u_2} {R : Type u_4} [DecidableEq ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike.GradedMonoid A] [Sub ι] [OrderedSub ι] [AddLeftReflectLE ι] (r : DirectSum ι fun i => ↥(A i)) {i : ι} (r' : ↥(A i)) (n : ι) [Decidable (i ≤ n)] : ↑((r * (DirectSum.of (fun i => ↥(A i)) i) r') n) = if i ≤ n then ↑(r (n - i)) * ↑r' else 0 - DirectSum.coe_of_mul_apply 📋 Mathlib.Algebra.DirectSum.Internal
{ι : Type u_1} {σ : Type u_2} {R : Type u_4} [DecidableEq ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike.GradedMonoid A] [Sub ι] [OrderedSub ι] [AddLeftReflectLE ι] {i : ι} (r : ↥(A i)) (r' : DirectSum ι fun i => ↥(A i)) (n : ι) [Decidable (i ≤ n)] : ↑(((DirectSum.of (fun i => ↥(A i)) i) r * r') n) = if i ≤ n then ↑r * ↑(r' (n - i)) else 0 - DirectSum.coe_decompose_mul_of_left_mem_of_le 📋 Mathlib.RingTheory.GradedAlgebra.Basic
{ι : Type u_1} {A : Type u_3} {σ : Type u_4} [Semiring A] [DecidableEq ι] [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] {a b : A} {n i : ι} [Sub ι] [OrderedSub ι] [AddLeftReflectLE ι] (a_mem : a ∈ 𝒜 i) (h : i ≤ n) : ↑(((DirectSum.decompose 𝒜) (a * b)) n) = a * ↑(((DirectSum.decompose 𝒜) b) (n - i)) - DirectSum.coe_decompose_mul_of_right_mem_of_le 📋 Mathlib.RingTheory.GradedAlgebra.Basic
{ι : Type u_1} {A : Type u_3} {σ : Type u_4} [Semiring A] [DecidableEq ι] [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] {a b : A} {n i : ι} [Sub ι] [OrderedSub ι] [AddLeftReflectLE ι] (b_mem : b ∈ 𝒜 i) (h : i ≤ n) : ↑(((DirectSum.decompose 𝒜) (a * b)) n) = ↑(((DirectSum.decompose 𝒜) a) (n - i)) * b - DirectSum.coe_decompose_mul_of_left_mem 📋 Mathlib.RingTheory.GradedAlgebra.Basic
{ι : Type u_1} {A : Type u_3} {σ : Type u_4} [Semiring A] [DecidableEq ι] [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] {a b : A} {i : ι} [Sub ι] [OrderedSub ι] [AddLeftReflectLE ι] (n : ι) [Decidable (i ≤ n)] (a_mem : a ∈ 𝒜 i) : ↑(((DirectSum.decompose 𝒜) (a * b)) n) = if i ≤ n then a * ↑(((DirectSum.decompose 𝒜) b) (n - i)) else 0 - DirectSum.coe_decompose_mul_of_right_mem 📋 Mathlib.RingTheory.GradedAlgebra.Basic
{ι : Type u_1} {A : Type u_3} {σ : Type u_4} [Semiring A] [DecidableEq ι] [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] {a b : A} {i : ι} [Sub ι] [OrderedSub ι] [AddLeftReflectLE ι] (n : ι) [Decidable (i ≤ n)] (b_mem : b ∈ 𝒜 i) : ↑(((DirectSum.decompose 𝒜) (a * b)) n) = if i ≤ n then ↑(((DirectSum.decompose 𝒜) a) (n - i)) * b else 0 - map_tsub_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Hom
{α : Type u_1} {β : Type u_2} {F : Type u_3} [PartialOrder α] [AddCommSemigroup α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] [PartialOrder β] [AddCommSemigroup β] [Sub β] [OrderedSub β] [AddLeftReflectLE β] [FunLike F α β] [AddHomClass F α β] (f : F) (a b : α) (h : b ≤ a) : f a - f b = f (a - b)
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