mathlib3 documentation

algebra.order.group.defs

Ordered groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file develops the basics of ordered groups.

Implementation details #

Unfortunately, the number of ' appended to lemmas in this file may differ between the multiplicative and the additive version of a lemma. The reason is that we did not want to change existing names in the library.

source
@[instance]
def ordered_add_comm_group.to_partial_order (α : Type u) [self : ordered_add_comm_group α] :
partial_order α
source
@[class]
structure ordered_add_comm_group (α : Type u) :
Type u

An ordered additive commutative group is an additive commutative group with a partial order in which addition is strictly monotone.

Instances of this typeclass
Instances of other typeclasses for ordered_add_comm_group
  • ordered_add_comm_group.has_sizeof_inst
source
@[instance]
def ordered_add_comm_group.to_add_comm_group (α : Type u) [self : ordered_add_comm_group α] :
add_comm_group α
source
@[instance]
def ordered_comm_group.to_comm_group (α : Type u) [self : ordered_comm_group α] :
comm_group α
source
@[class]
structure ordered_comm_group (α : Type u) :
Type u

An ordered commutative group is an commutative group with a partial order in which multiplication is strictly monotone.

Instances of this typeclass
Instances of other typeclasses for ordered_comm_group
  • ordered_comm_group.has_sizeof_inst
source
@[instance]
def ordered_comm_group.to_partial_order (α : Type u) [self : ordered_comm_group α] :
partial_order α
source
@[protected, instance]
def ordered_add_comm_group.to_covariant_class_left_le (α : Type u) [ordered_add_comm_group α] :
covariant_class α α has_add.add has_le.le
source
@[protected, instance]
def ordered_comm_group.to_covariant_class_left_le (α : Type u) [ordered_comm_group α] :
covariant_class α α has_mul.mul has_le.le
source
@[protected, instance]
def ordered_add_comm_group.to_ordered_cancel_add_comm_monoid {α : Type u} [ordered_add_comm_group α] :
ordered_cancel_add_comm_monoid α
Equations
source
@[protected, instance]
def ordered_comm_group.to_ordered_cancel_comm_monoid {α : Type u} [ordered_comm_group α] :
ordered_cancel_comm_monoid α
Equations
source
theorem ordered_add_comm_group.to_contravariant_class_left_le (α : Type u) [ordered_add_comm_group α] :
contravariant_class α α has_add.add has_le.le

A choice-free shortcut instance.

source
theorem ordered_comm_group.to_contravariant_class_left_le (α : Type u) [ordered_comm_group α] :
contravariant_class α α has_mul.mul has_le.le

A choice-free shortcut instance.

source
theorem ordered_comm_group.to_contravariant_class_right_le (α : Type u) [ordered_comm_group α] :
contravariant_class α α (function.swap has_mul.mul) has_le.le

A choice-free shortcut instance.

source
theorem ordered_add_comm_group.to_contravariant_class_right_le (α : Type u) [ordered_add_comm_group α] :
contravariant_class α α (function.swap has_add.add) has_le.le

A choice-free shortcut instance.

source
@[simp]
theorem left.neg_nonpos_iff {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a : α} :
-a ≤ 0 ↔ 0 ≤ a

Uses left co(ntra)variant.

source
@[simp]
theorem left.inv_le_one_iff {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a : α} :
a⁻¹ ≤ 1 ↔ 1 ≤ a

Uses left co(ntra)variant.

source
@[simp]
theorem left.nonneg_neg_iff {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a : α} :
0 ≤ -a ↔ a ≤ 0

Uses left co(ntra)variant.

source
@[simp]
theorem left.one_le_inv_iff {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a : α} :
1 ≤ a⁻¹ ↔ a ≤ 1

Uses left co(ntra)variant.

source
@[simp]
theorem le_neg_add_iff_add_le {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
b ≤ -a + c ↔ a + b ≤ c
source
@[simp]
theorem le_inv_mul_iff_mul_le {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} :
b ≤ a⁻¹ * c ↔ a * b ≤ c
source
@[simp]
theorem inv_mul_le_iff_le_mul {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} :
b⁻¹ * a ≤ c ↔ a ≤ b * c
source
@[simp]
theorem neg_add_le_iff_le_add {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
-b + a ≤ c ↔ a ≤ b + c
source
theorem inv_le_iff_one_le_mul' {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b : α} :
a⁻¹ ≤ b ↔ 1 ≤ a * b
source
theorem neg_le_iff_add_nonneg' {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b : α} :
-a ≤ b ↔ 0 ≤ a + b
source
theorem le_inv_iff_mul_le_one_left {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b : α} :
a ≤ b⁻¹ ↔ b * a ≤ 1
source
theorem le_neg_iff_add_nonpos_left {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b : α} :
a ≤ -b ↔ b + a ≤ 0
source
theorem le_neg_add_iff_le {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b : α} :
0 ≤ -b + a ↔ b ≤ a
source
theorem le_inv_mul_iff_le {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b : α} :
1 ≤ b⁻¹ * a ↔ b ≤ a
source
theorem neg_add_nonpos_iff {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b : α} :
-a + b ≤ 0 ↔ b ≤ a
source
theorem inv_mul_le_one_iff {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b : α} :
a⁻¹ * b ≤ 1 ↔ b ≤ a
source
@[simp]
theorem left.one_lt_inv_iff {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a : α} :
1 < a⁻¹ ↔ a < 1

Uses left co(ntra)variant.

source
@[simp]
theorem left.neg_pos_iff {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a : α} :
0 < -a ↔ a < 0

Uses left co(ntra)variant.

source
@[simp]
theorem left.neg_neg_iff {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a : α} :
-a < 0 ↔ 0 < a

Uses left co(ntra)variant.

source
@[simp]
theorem left.inv_lt_one_iff {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a : α} :
a⁻¹ < 1 ↔ 1 < a

Uses left co(ntra)variant.

source
@[simp]
theorem lt_inv_mul_iff_mul_lt {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
b < a⁻¹ * c ↔ a * b < c
source
@[simp]
theorem lt_neg_add_iff_add_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
b < -a + c ↔ a + b < c
source
@[simp]
theorem inv_mul_lt_iff_lt_mul {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
b⁻¹ * a < c ↔ a < b * c
source
@[simp]
theorem neg_add_lt_iff_lt_add {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
-b + a < c ↔ a < b + c
source
theorem inv_lt_iff_one_lt_mul' {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b : α} :
a⁻¹ < b ↔ 1 < a * b
source
theorem neg_lt_iff_pos_add' {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b : α} :
-a < b ↔ 0 < a + b
source
theorem lt_inv_iff_mul_lt_one' {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b : α} :
a < b⁻¹ ↔ b * a < 1
source
theorem lt_neg_iff_add_neg' {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b : α} :
a < -b ↔ b + a < 0
source
theorem lt_inv_mul_iff_lt {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b : α} :
1 < b⁻¹ * a ↔ b < a
source
theorem lt_neg_add_iff_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b : α} :
0 < -b + a ↔ b < a
source
theorem inv_mul_lt_one_iff {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b : α} :
a⁻¹ * b < 1 ↔ b < a
source
theorem neg_add_neg_iff {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b : α} :
-a + b < 0 ↔ b < a
source
@[simp]
theorem right.neg_nonpos_iff {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a : α} :
-a ≤ 0 ↔ 0 ≤ a

Uses right co(ntra)variant.

source
@[simp]
theorem right.inv_le_one_iff {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a : α} :
a⁻¹ ≤ 1 ↔ 1 ≤ a

Uses right co(ntra)variant.

source
@[simp]
theorem right.nonneg_neg_iff {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a : α} :
0 ≤ -a ↔ a ≤ 0

Uses right co(ntra)variant.

source
@[simp]
theorem right.one_le_inv_iff {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a : α} :
1 ≤ a⁻¹ ↔ a ≤ 1

Uses right co(ntra)variant.

source
theorem inv_le_iff_one_le_mul {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} :
a⁻¹ ≤ b ↔ 1 ≤ b * a
source
theorem neg_le_iff_add_nonneg {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
-a ≤ b ↔ 0 ≤ b + a
source
theorem le_neg_iff_add_nonpos_right {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
a ≤ -b ↔ a + b ≤ 0
source
theorem le_inv_iff_mul_le_one_right {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} :
a ≤ b⁻¹ ↔ a * b ≤ 1
source
@[simp]
theorem mul_inv_le_iff_le_mul {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c : α} :
a * b⁻¹ ≤ c ↔ a ≤ c * b
source
@[simp]
theorem add_neg_le_iff_le_add {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} :
a + -b ≤ c ↔ a ≤ c + b
source
@[simp]
theorem le_mul_inv_iff_mul_le {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c : α} :
c ≤ a * b⁻¹ ↔ c * b ≤ a
source
@[simp]
theorem le_add_neg_iff_add_le {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} :
c ≤ a + -b ↔ c + b ≤ a
source
@[simp]
theorem mul_inv_le_one_iff_le {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} :
a * b⁻¹ ≤ 1 ↔ a ≤ b
source
@[simp]
theorem add_neg_nonpos_iff_le {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
a + -b ≤ 0 ↔ a ≤ b
source
theorem le_add_neg_iff_le {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
0 ≤ a + -b ↔ b ≤ a
source
theorem le_mul_inv_iff_le {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} :
1 ≤ a * b⁻¹ ↔ b ≤ a
source
theorem mul_inv_le_one_iff {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} :
b * a⁻¹ ≤ 1 ↔ b ≤ a
source
theorem add_neg_nonpos_iff {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
b + -a ≤ 0 ↔ b ≤ a
source
@[simp]
theorem right.neg_neg_iff {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a : α} :
-a < 0 ↔ 0 < a

Uses right co(ntra)variant.

source
@[simp]
theorem right.inv_lt_one_iff {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a : α} :
a⁻¹ < 1 ↔ 1 < a

Uses right co(ntra)variant.

source
@[simp]
theorem right.one_lt_inv_iff {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a : α} :
1 < a⁻¹ ↔ a < 1

Uses right co(ntra)variant.

source
@[simp]
theorem right.neg_pos_iff {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a : α} :
0 < -a ↔ a < 0

Uses right co(ntra)variant.

source
theorem neg_lt_iff_pos_add {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
-a < b ↔ 0 < b + a
source
theorem inv_lt_iff_one_lt_mul {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} :
a⁻¹ < b ↔ 1 < b * a
source
theorem lt_inv_iff_mul_lt_one {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} :
a < b⁻¹ ↔ a * b < 1
source
theorem lt_neg_iff_add_neg {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
a < -b ↔ a + b < 0
source
@[simp]
theorem mul_inv_lt_iff_lt_mul {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b c : α} :
a * b⁻¹ < c ↔ a < c * b
source
@[simp]
theorem add_neg_lt_iff_lt_add {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} :
a + -b < c ↔ a < c + b
source
@[simp]
theorem lt_add_neg_iff_add_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} :
c < a + -b ↔ c + b < a
source
@[simp]
theorem lt_mul_inv_iff_mul_lt {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b c : α} :
c < a * b⁻¹ ↔ c * b < a
source
@[simp]
theorem neg_add_neg_iff_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
a + -b < 0 ↔ a < b
source
@[simp]
theorem inv_mul_lt_one_iff_lt {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} :
a * b⁻¹ < 1 ↔ a < b
source
theorem lt_mul_inv_iff_lt {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} :
1 < a * b⁻¹ ↔ b < a
source
theorem lt_add_neg_iff_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
0 < a + -b ↔ b < a
source
theorem add_neg_neg_iff {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
b + -a < 0 ↔ b < a
source
theorem mul_inv_lt_one_iff {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} :
b * a⁻¹ < 1 ↔ b < a
source
@[simp]
theorem neg_le_neg_iff {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
-a ≤ -b ↔ b ≤ a
source
@[simp]
theorem inv_le_inv_iff {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} :
a⁻¹ ≤ b⁻¹ ↔ b ≤ a
source
theorem le_of_neg_le_neg {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
-a ≤ -b → b ≤ a

Alias of the forward direction of neg_le_neg_iff.

source
theorem mul_inv_le_inv_mul_iff {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c d : α} :
a * b⁻¹ ≤ d⁻¹ * c ↔ d * a ≤ c * b
source
theorem add_neg_le_neg_add_iff {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c d : α} :
a + -b ≤ -d + c ↔ d + a ≤ c + b
source
@[simp]
theorem sub_le_self_iff {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (a : α) {b : α} :
a - b ≤ a ↔ 0 ≤ b
source
@[simp]
theorem div_le_self_iff {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a : α) {b : α} :
a / b ≤ a ↔ 1 ≤ b
source
@[simp]
theorem le_sub_self_iff {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (a : α) {b : α} :
a ≤ a - b ↔ b ≤ 0
source
@[simp]
theorem le_div_self_iff {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a : α) {b : α} :
a ≤ a / b ↔ b ≤ 1
source
theorem sub_le_self {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (a : α) {b : α} :
0 ≤ b → a - b ≤ a

Alias of the reverse direction of sub_le_self_iff.

source
@[simp]
theorem inv_lt_inv_iff {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} :
a⁻¹ < b⁻¹ ↔ b < a
source
@[simp]
theorem neg_lt_neg_iff {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
-a < -b ↔ b < a
source
theorem neg_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
-a < b ↔ -b < a
source
theorem inv_lt' {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} :
a⁻¹ < b ↔ b⁻¹ < a
source
theorem lt_inv' {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} :
a < b⁻¹ ↔ b < a⁻¹
source
theorem lt_neg {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
a < -b ↔ b < -a
source
theorem lt_inv_of_lt_inv {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} :
a < b⁻¹ → b < a⁻¹

Alias of the forward direction of lt_inv'.

source
theorem lt_neg_of_lt_neg {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
a < -b → b < -a

Alias of the forward direction of lt_inv'.

source
theorem inv_lt_of_inv_lt' {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} :
a⁻¹ < b → b⁻¹ < a

Alias of the forward direction of inv_lt'.

source
theorem neg_lt_of_neg_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
-a < b → -b < a

Alias of the forward direction of inv_lt'.

source
theorem mul_inv_lt_inv_mul_iff {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b c d : α} :
a * b⁻¹ < d⁻¹ * c ↔ d * a < c * b
source
theorem add_neg_lt_neg_add_iff {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c d : α} :
a + -b < -d + c ↔ d + a < c + b
source
@[simp]
theorem div_lt_self_iff {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] (a : α) {b : α} :
a / b < a ↔ 1 < b
source
@[simp]
theorem sub_lt_self_iff {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] (a : α) {b : α} :
a - b < a ↔ 0 < b
source
theorem sub_lt_self {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] (a : α) {b : α} :
0 < b → a - b < a

Alias of the reverse direction of sub_lt_self_iff.

source
theorem left.neg_le_self {α : Type u} [add_group α] [preorder α] [covariant_class α α has_add.add has_le.le] {a : α} (h : 0 ≤ a) :
-a ≤ a
source
theorem left.inv_le_self {α : Type u} [group α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a : α} (h : 1 ≤ a) :
a⁻¹ ≤ a
source
theorem neg_le_self {α : Type u} [add_group α] [preorder α] [covariant_class α α has_add.add has_le.le] {a : α} (h : 0 ≤ a) :
-a ≤ a

Alias of left.neg_le_self.

source
theorem left.self_le_neg {α : Type u} [add_group α] [preorder α] [covariant_class α α has_add.add has_le.le] {a : α} (h : a ≤ 0) :
a ≤ -a
source
theorem left.self_le_inv {α : Type u} [group α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a : α} (h : a ≤ 1) :
a ≤ a⁻¹
source
theorem left.inv_lt_self {α : Type u} [group α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] {a : α} (h : 1 < a) :
a⁻¹ < a
source
theorem left.neg_lt_self {α : Type u} [add_group α] [preorder α] [covariant_class α α has_add.add has_lt.lt] {a : α} (h : 0 < a) :
-a < a
source
theorem neg_lt_self {α : Type u} [add_group α] [preorder α] [covariant_class α α has_add.add has_lt.lt] {a : α} (h : 0 < a) :
-a < a

Alias of left.neg_lt_self.

source
theorem left.self_lt_neg {α : Type u} [add_group α] [preorder α] [covariant_class α α has_add.add has_lt.lt] {a : α} (h : a < 0) :
a < -a
source
theorem left.self_lt_inv {α : Type u} [group α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] {a : α} (h : a < 1) :
a < a⁻¹
source
theorem right.neg_le_self {α : Type u} [add_group α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {a : α} (h : 0 ≤ a) :
-a ≤ a
source
theorem right.inv_le_self {α : Type u} [group α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a : α} (h : 1 ≤ a) :
a⁻¹ ≤ a
source
theorem right.self_le_neg {α : Type u} [add_group α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {a : α} (h : a ≤ 0) :
a ≤ -a
source
theorem right.self_le_inv {α : Type u} [group α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a : α} (h : a ≤ 1) :
a ≤ a⁻¹
source
theorem right.neg_lt_self {α : Type u} [add_group α] [preorder α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a : α} (h : 0 < a) :
-a < a
source
theorem right.inv_lt_self {α : Type u} [group α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a : α} (h : 1 < a) :
a⁻¹ < a
source
theorem right.self_lt_inv {α : Type u} [group α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a : α} (h : a < 1) :
a < a⁻¹
source
theorem right.self_lt_neg {α : Type u} [add_group α] [preorder α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a : α} (h : a < 0) :
a < -a
source
theorem inv_mul_le_iff_le_mul' {α : Type u} [comm_group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} :
c⁻¹ * a ≤ b ↔ a ≤ b * c
source
theorem neg_add_le_iff_le_add' {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
-c + a ≤ b ↔ a ≤ b + c
source
@[simp]
theorem mul_inv_le_iff_le_mul' {α : Type u} [comm_group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} :
a * b⁻¹ ≤ c ↔ a ≤ b * c
source
@[simp]
theorem add_neg_le_iff_le_add' {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
a + -b ≤ c ↔ a ≤ b + c
source
theorem add_neg_le_add_neg_iff {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c d : α} :
a + -b ≤ c + -d ↔ a + d ≤ c + b
source
theorem mul_inv_le_mul_inv_iff' {α : Type u} [comm_group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c d : α} :
a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b
source
theorem neg_add_lt_iff_lt_add' {α : Type u} [add_comm_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
-c + a < b ↔ a < b + c
source
theorem inv_mul_lt_iff_lt_mul' {α : Type u} [comm_group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
c⁻¹ * a < b ↔ a < b * c
source
@[simp]
theorem mul_inv_lt_iff_le_mul' {α : Type u} [comm_group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
a * b⁻¹ < c ↔ a < b * c
source
@[simp]
theorem add_neg_lt_iff_le_add' {α : Type u} [add_comm_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
a + -b < c ↔ a < b + c
source
theorem add_neg_lt_add_neg_iff {α : Type u} [add_comm_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c d : α} :
a + -b < c + -d ↔ a + d < c + b
source
theorem mul_inv_lt_mul_inv_iff' {α : Type u} [comm_group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c d : α} :
a * b⁻¹ < c * d⁻¹ ↔ a * d < c * b
source
theorem one_le_of_inv_le_one {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a : α} :
a⁻¹ ≤ 1 → 1 ≤ a

Alias of the forward direction of left.inv_le_one_iff.

source
theorem nonneg_of_neg_nonpos {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a : α} :
-a ≤ 0 → 0 ≤ a

Alias of the forward direction of left.inv_le_one_iff.

source
theorem le_one_of_one_le_inv {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a : α} :
1 ≤ a⁻¹ → a ≤ 1

Alias of the forward direction of left.one_le_inv_iff.

source
theorem nonpos_of_neg_nonneg {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a : α} :
0 ≤ -a → a ≤ 0

Alias of the forward direction of left.one_le_inv_iff.

source
theorem lt_of_inv_lt_inv {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} :
a⁻¹ < b⁻¹ → b < a

Alias of the forward direction of inv_lt_inv_iff.

source
theorem lt_of_neg_lt_neg {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
-a < -b → b < a

Alias of the forward direction of inv_lt_inv_iff.

source
theorem one_lt_of_inv_lt_one {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a : α} :
a⁻¹ < 1 → 1 < a

Alias of the forward direction of left.inv_lt_one_iff.

source
theorem pos_of_neg_neg {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a : α} :
-a < 0 → 0 < a

Alias of the forward direction of left.inv_lt_one_iff.

source
theorem inv_lt_one_iff_one_lt {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a : α} :
a⁻¹ < 1 ↔ 1 < a

Alias of left.inv_lt_one_iff.

source
theorem neg_neg_iff_pos {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a : α} :
-a < 0 ↔ 0 < a

Alias of left.inv_lt_one_iff.

source
theorem inv_lt_one' {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a : α} :
a⁻¹ < 1 ↔ 1 < a

Alias of left.inv_lt_one_iff.

source
theorem neg_lt_zero {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a : α} :
-a < 0 ↔ 0 < a

Alias of left.inv_lt_one_iff.

source
theorem inv_of_one_lt_inv {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a : α} :
1 < a⁻¹ → a < 1

Alias of the forward direction of left.one_lt_inv_iff.

source
theorem neg_of_neg_pos {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a : α} :
0 < -a → a < 0

Alias of the forward direction of left.one_lt_inv_iff.

source
theorem one_lt_inv_of_inv {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a : α} :
a < 1 → 1 < a⁻¹

Alias of the reverse direction of left.one_lt_inv_iff.

source
theorem neg_pos_of_neg {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a : α} :
a < 0 → 0 < -a

Alias of the reverse direction of left.one_lt_inv_iff.

source
theorem mul_le_of_le_inv_mul {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} :
b ≤ a⁻¹ * c → a * b ≤ c

Alias of the forward direction of le_inv_mul_iff_mul_le.

source
theorem add_le_of_le_neg_add {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
b ≤ -a + c → a + b ≤ c

Alias of the forward direction of le_inv_mul_iff_mul_le.

source
theorem le_inv_mul_of_mul_le {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} :
a * b ≤ c → b ≤ a⁻¹ * c

Alias of the reverse direction of le_inv_mul_iff_mul_le.

source
theorem le_neg_add_of_add_le {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
a + b ≤ c → b ≤ -a + c

Alias of the reverse direction of le_inv_mul_iff_mul_le.

source
theorem inv_mul_le_of_le_mul {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} :
a ≤ b * c → b⁻¹ * a ≤ c

Alias of the reverse direction of inv_mul_le_iff_le_mul.

source
theorem mul_lt_of_lt_inv_mul {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
b < a⁻¹ * c → a * b < c

Alias of the forward direction of lt_inv_mul_iff_mul_lt.

source
theorem add_lt_of_lt_neg_add {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
b < -a + c → a + b < c

Alias of the forward direction of lt_inv_mul_iff_mul_lt.

source
theorem lt_inv_mul_of_mul_lt {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
a * b < c → b < a⁻¹ * c

Alias of the reverse direction of lt_inv_mul_iff_mul_lt.

source
theorem lt_neg_add_of_add_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
a + b < c → b < -a + c

Alias of the reverse direction of lt_inv_mul_iff_mul_lt.

source
theorem inv_mul_lt_of_lt_mul {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
a < b * c → b⁻¹ * a < c

Alias of the reverse direction of inv_mul_lt_iff_lt_mul.

source
theorem lt_mul_of_inv_mul_lt {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
b⁻¹ * a < c → a < b * c

Alias of the forward direction of inv_mul_lt_iff_lt_mul.

source
theorem lt_add_of_neg_add_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
-b + a < c → a < b + c

Alias of the forward direction of inv_mul_lt_iff_lt_mul.

source
theorem neg_add_lt_of_lt_add {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
a < b + c → -b + a < c

Alias of the reverse direction of inv_mul_lt_iff_lt_mul.

source
theorem lt_mul_of_inv_mul_lt_left {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
b⁻¹ * a < c → a < b * c

Alias of lt_mul_of_inv_mul_lt.

source
theorem lt_add_of_neg_add_lt_left {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
-b + a < c → a < b + c

Alias of lt_mul_of_inv_mul_lt.

source
theorem inv_le_one' {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a : α} :
a⁻¹ ≤ 1 ↔ 1 ≤ a

Alias of left.inv_le_one_iff.

source
theorem neg_nonpos {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a : α} :
-a ≤ 0 ↔ 0 ≤ a

Alias of left.inv_le_one_iff.

source
theorem one_le_inv' {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a : α} :
1 ≤ a⁻¹ ↔ a ≤ 1

Alias of left.one_le_inv_iff.

source
theorem neg_nonneg {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a : α} :
0 ≤ -a ↔ a ≤ 0

Alias of left.one_le_inv_iff.

source
theorem one_lt_inv' {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a : α} :
1 < a⁻¹ ↔ a < 1

Alias of left.one_lt_inv_iff.

source
theorem neg_pos {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a : α} :
0 < -a ↔ a < 0

Alias of left.one_lt_inv_iff.

source
theorem ordered_comm_group.mul_lt_mul_left' {α : Type u_1} [has_mul α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {b c : α} (bc : b < c) (a : α) :
a * b < a * c

Alias of mul_lt_mul_left'.

source
theorem ordered_add_comm_group.add_lt_add_left {α : Type u_1} [has_add α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {b c : α} (bc : b < c) (a : α) :
a + b < a + c

Alias of mul_lt_mul_left'.

source
theorem ordered_comm_group.le_of_mul_le_mul_left {α : Type u_1} [has_mul α] [has_le α] [contravariant_class α α has_mul.mul has_le.le] {a b c : α} (bc : a * b ≤ a * c) :
b ≤ c

Alias of le_of_mul_le_mul_left'.

source
theorem ordered_add_comm_group.le_of_add_le_add_left {α : Type u_1} [has_add α] [has_le α] [contravariant_class α α has_add.add has_le.le] {a b c : α} (bc : a + b ≤ a + c) :
b ≤ c

Alias of le_of_mul_le_mul_left'.

source
theorem ordered_comm_group.lt_of_mul_lt_mul_left {α : Type u_1} [has_mul α] [has_lt α] [contravariant_class α α has_mul.mul has_lt.lt] {a b c : α} (bc : a * b < a * c) :
b < c

Alias of lt_of_mul_lt_mul_left'.

source
theorem ordered_add_comm_group.lt_of_add_lt_add_left {α : Type u_1} [has_add α] [has_lt α] [contravariant_class α α has_add.add has_lt.lt] {a b c : α} (bc : a + b < a + c) :
b < c

Alias of lt_of_mul_lt_mul_left'.

source
@[simp]
theorem div_le_div_iff_right {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} (c : α) :
a / c ≤ b / c ↔ a ≤ b
source
@[simp]
theorem sub_le_sub_iff_right {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} (c : α) :
a - c ≤ b - c ↔ a ≤ b
source
theorem sub_le_sub_right {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} (h : a ≤ b) (c : α) :
a - c ≤ b - c
source
theorem div_le_div_right' {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} (h : a ≤ b) (c : α) :
a / c ≤ b / c
source
@[simp]
theorem sub_nonneg {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
0 ≤ a - b ↔ b ≤ a
source
@[simp]
theorem one_le_div' {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} :
1 ≤ a / b ↔ b ≤ a
source
theorem le_of_sub_nonneg {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
0 ≤ a - b → b ≤ a

Alias of the forward direction of sub_nonneg.

source
theorem sub_nonneg_of_le {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
b ≤ a → 0 ≤ a - b

Alias of the reverse direction of sub_nonneg.

source
@[simp]
theorem div_le_one' {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} :
a / b ≤ 1 ↔ a ≤ b
source
@[simp]
theorem sub_nonpos {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
a - b ≤ 0 ↔ a ≤ b
source
theorem sub_nonpos_of_le {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
a ≤ b → a - b ≤ 0

Alias of the reverse direction of sub_nonpos.

source
theorem le_of_sub_nonpos {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
a - b ≤ 0 → a ≤ b

Alias of the forward direction of sub_nonpos.

source
theorem le_div_iff_mul_le {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c : α} :
a ≤ c / b ↔ a * b ≤ c
source
theorem le_sub_iff_add_le {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} :
a ≤ c - b ↔ a + b ≤ c
source
theorem add_le_of_le_sub_right {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} :
a ≤ c - b → a + b ≤ c

Alias of the forward direction of le_sub_iff_add_le.

source
theorem le_sub_right_of_add_le {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} :
a + b ≤ c → a ≤ c - b

Alias of the reverse direction of le_sub_iff_add_le.

source
theorem sub_le_iff_le_add {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} :
a - c ≤ b ↔ a ≤ b + c
source
theorem div_le_iff_le_mul {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c : α} :
a / c ≤ b ↔ a ≤ b * c
source
@[protected, instance]
def add_group.to_has_ordered_sub {α : Type u_1} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] :
has_ordered_sub α
source
@[simp]
theorem div_le_div_iff_left {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] {b c : α} (a : α) :
a / b ≤ a / c ↔ c ≤ b
source
@[simp]
theorem sub_le_sub_iff_left {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] {b c : α} (a : α) :
a - b ≤ a - c ↔ c ≤ b
source
theorem div_le_div_left' {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} (h : a ≤ b) (c : α) :
c / b ≤ c / a
source
theorem sub_le_sub_left {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} (h : a ≤ b) (c : α) :
c - b ≤ c - a
source
theorem sub_le_sub_iff {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c d : α} :
a - b ≤ c - d ↔ a + d ≤ c + b
source
theorem div_le_div_iff' {α : Type u} [comm_group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c d : α} :
a / b ≤ c / d ↔ a * d ≤ c * b
source
theorem le_sub_iff_add_le' {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
b ≤ c - a ↔ a + b ≤ c
source
theorem le_div_iff_mul_le' {α : Type u} [comm_group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} :
b ≤ c / a ↔ a * b ≤ c
source
theorem add_le_of_le_sub_left {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
b ≤ c - a → a + b ≤ c

Alias of the forward direction of le_sub_iff_add_le'.

source
theorem le_sub_left_of_add_le {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
a + b ≤ c → b ≤ c - a

Alias of the reverse direction of le_sub_iff_add_le'.

source
theorem sub_le_iff_le_add' {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
a - b ≤ c ↔ a ≤ b + c
source
theorem div_le_iff_le_mul' {α : Type u} [comm_group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} :
a / b ≤ c ↔ a ≤ b * c
source
theorem le_add_of_sub_left_le {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
a - b ≤ c → a ≤ b + c

Alias of the forward direction of sub_le_iff_le_add'.

source
theorem sub_left_le_of_le_add {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
a ≤ b + c → a - b ≤ c

Alias of the reverse direction of sub_le_iff_le_add'.

source
@[simp]
theorem neg_le_sub_iff_le_add {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
-b ≤ a - c ↔ c ≤ a + b
source
@[simp]
theorem inv_le_div_iff_le_mul {α : Type u} [comm_group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} :
b⁻¹ ≤ a / c ↔ c ≤ a * b
source
theorem inv_le_div_iff_le_mul' {α : Type u} [comm_group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} :
a⁻¹ ≤ b / c ↔ c ≤ a * b
source
theorem neg_le_sub_iff_le_add' {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
-a ≤ b - c ↔ c ≤ a + b
source
theorem sub_le_comm {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
a - b ≤ c ↔ a - c ≤ b
source
theorem div_le_comm {α : Type u} [comm_group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} :
a / b ≤ c ↔ a / c ≤ b
source
theorem le_div_comm {α : Type u} [comm_group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} :
a ≤ b / c ↔ c ≤ b / a
source
theorem le_sub_comm {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
a ≤ b - c ↔ c ≤ b - a
source
theorem div_le_div'' {α : Type u} [comm_group α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b c d : α} (hab : a ≤ b) (hcd : c ≤ d) :
a / d ≤ b / c
source
theorem sub_le_sub {α : Type u} [add_comm_group α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b c d : α} (hab : a ≤ b) (hcd : c ≤ d) :
a - d ≤ b - c
source
@[simp]
theorem sub_lt_sub_iff_right {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} (c : α) :
a - c < b - c ↔ a < b
source
@[simp]
theorem div_lt_div_iff_right {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} (c : α) :
a / c < b / c ↔ a < b
source
theorem div_lt_div_right' {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} (h : a < b) (c : α) :
a / c < b / c
source
theorem sub_lt_sub_right {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} (h : a < b) (c : α) :
a - c < b - c
source
@[simp]
theorem sub_pos {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
0 < a - b ↔ b < a
source
@[simp]
theorem one_lt_div' {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} :
1 < a / b ↔ b < a
source
theorem lt_of_sub_pos {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
0 < a - b → b < a

Alias of the forward direction of sub_pos.

source
theorem sub_pos_of_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
b < a → 0 < a - b

Alias of the reverse direction of sub_pos.

source
@[simp]
theorem div_lt_one' {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} :
a / b < 1 ↔ a < b
source
@[simp]
theorem sub_neg {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
a - b < 0 ↔ a < b
source
theorem lt_of_sub_neg {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
a - b < 0 → a < b

Alias of the forward direction of sub_neg.

source
theorem sub_neg_of_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
a < b → a - b < 0

Alias of the reverse direction of sub_neg.

source
theorem sub_lt_zero {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
a - b < 0 ↔ a < b

Alias of sub_neg.

source
theorem lt_sub_iff_add_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} :
a < c - b ↔ a + b < c
source
theorem lt_div_iff_mul_lt {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b c : α} :
a < c / b ↔ a * b < c
source
theorem add_lt_of_lt_sub_right {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} :
a < c - b → a + b < c

Alias of the forward direction of lt_sub_iff_add_lt.

source
theorem lt_sub_right_of_add_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} :
a + b < c → a < c - b

Alias of the reverse direction of lt_sub_iff_add_lt.

source
theorem sub_lt_iff_lt_add {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} :
a - c < b ↔ a < b + c
source
theorem div_lt_iff_lt_mul {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b c : α} :
a / c < b ↔ a < b * c
source
theorem lt_add_of_sub_right_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} :
a - c < b → a < b + c

Alias of the forward direction of sub_lt_iff_lt_add.

source
theorem sub_right_lt_of_lt_add {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} :
a < b + c → a - c < b

Alias of the reverse direction of sub_lt_iff_lt_add.

source
@[simp]
theorem div_lt_div_iff_left {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {b c : α} (a : α) :
a / b < a / c ↔ c < b
source
@[simp]
theorem sub_lt_sub_iff_left {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] {b c : α} (a : α) :
a - b < a - c ↔ c < b
source
@[simp]
theorem neg_lt_sub_iff_lt_add {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} :
-a < b - c ↔ c < a + b
source
@[simp]
theorem inv_lt_div_iff_lt_mul {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b c : α} :
a⁻¹ < b / c ↔ c < a * b
source
theorem sub_lt_sub_left {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} (h : a < b) (c : α) :
c - b < c - a
source
theorem div_lt_div_left' {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} (h : a < b) (c : α) :
c / b < c / a
source
theorem div_lt_div_iff' {α : Type u} [comm_group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c d : α} :
a / b < c / d ↔ a * d < c * b
source
theorem sub_lt_sub_iff {α : Type u} [add_comm_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c d : α} :
a - b < c - d ↔ a + d < c + b
source
theorem lt_div_iff_mul_lt' {α : Type u} [comm_group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
b < c / a ↔ a * b < c
source
theorem lt_sub_iff_add_lt' {α : Type u} [add_comm_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
b < c - a ↔ a + b < c
source
theorem add_lt_of_lt_sub_left {α : Type u} [add_comm_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
b < c - a → a + b < c

Alias of the forward direction of lt_sub_iff_add_lt'.

source
theorem lt_sub_left_of_add_lt {α : Type u} [add_comm_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
a + b < c → b < c - a

Alias of the reverse direction of lt_sub_iff_add_lt'.

source
theorem div_lt_iff_lt_mul' {α : Type u} [comm_group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
a / b < c ↔ a < b * c
source
theorem sub_lt_iff_lt_add' {α : Type u} [add_comm_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
a - b < c ↔ a < b + c
source
theorem sub_left_lt_of_lt_add {α : Type u} [add_comm_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
a < b + c → a - b < c

Alias of the reverse direction of sub_lt_iff_lt_add'.

source
theorem lt_add_of_sub_left_lt {α : Type u} [add_comm_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
a - b < c → a < b + c

Alias of the forward direction of sub_lt_iff_lt_add'.

source
theorem inv_lt_div_iff_lt_mul' {α : Type u} [comm_group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
b⁻¹ < a / c ↔ c < a * b
source
theorem neg_lt_sub_iff_lt_add' {α : Type u} [add_comm_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
-b < a - c ↔ c < a + b
source
theorem div_lt_comm {α : Type u} [comm_group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
a / b < c ↔ a / c < b
source
theorem sub_lt_comm {α : Type u} [add_comm_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
a - b < c ↔ a - c < b
source
theorem lt_div_comm {α : Type u} [comm_group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
a < b / c ↔ c < b / a
source
theorem lt_sub_comm {α : Type u} [add_comm_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
a < b - c ↔ c < b - a
source
theorem div_lt_div'' {α : Type u} [comm_group α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] {a b c d : α} (hab : a < b) (hcd : c < d) :
a / d < b / c
source
theorem sub_lt_sub {α : Type u} [add_comm_group α] [preorder α] [covariant_class α α has_add.add has_lt.lt] {a b c d : α} (hab : a < b) (hcd : c < d) :
a - d < b - c
source
@[simp]
theorem cmp_sub_zero {α : Type u} [add_group α] [linear_order α] [covariant_class α α (function.swap has_add.add) has_le.le] (a b : α) :
cmp (a - b) 0 = cmp a b
source
@[simp]
theorem cmp_div_one' {α : Type u} [group α] [linear_order α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a b : α) :
cmp (a / b) 1 = cmp a b
source
theorem le_of_forall_one_lt_lt_mul {α : Type u} [group α] [linear_order α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (h : ∀ (ε : α), 1 < ε → a < b * ε) :
a ≤ b
source
theorem le_of_forall_pos_lt_add {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a b : α} (h : ∀ (ε : α), 0 < ε → a < b + ε) :
a ≤ b
source
theorem le_iff_forall_pos_lt_add {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a b : α} :
a ≤ b ↔ ∀ (ε : α), 0 < ε → a < b + ε
source
theorem le_iff_forall_one_lt_lt_mul {α : Type u} [group α] [linear_order α] [covariant_class α α has_mul.mul has_le.le] {a b : α} :
a ≤ b ↔ ∀ (ε : α), 1 < ε → a < b * ε
source
theorem sub_le_neg_add_iff {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a b : α} [covariant_class α α (function.swap has_add.add) has_le.le] :
a - b ≤ -a + b ↔ a ≤ b
source
theorem div_le_inv_mul_iff {α : Type u} [group α] [linear_order α] [covariant_class α α has_mul.mul has_le.le] {a b : α} [covariant_class α α (function.swap has_mul.mul) has_le.le] :
a / b ≤ a⁻¹ * b ↔ a ≤ b
source
@[simp]
theorem sub_le_sub_flip {α : Type u_1} [add_comm_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a b : α} :
a - b ≤ b - a ↔ a ≤ b
source
@[simp]
theorem div_le_div_flip {α : Type u_1} [comm_group α] [linear_order α] [covariant_class α α has_mul.mul has_le.le] {a b : α} :
a / b ≤ b / a ↔ a ≤ b

Linearly ordered commutative groups #

source
@[instance]
def linear_ordered_add_comm_group.to_linear_order (α : Type u) [self : linear_ordered_add_comm_group α] :
linear_order α
source
@[instance]
def linear_ordered_add_comm_group.to_ordered_add_comm_group (α : Type u) [self : linear_ordered_add_comm_group α] :
ordered_add_comm_group α
source
@[class]
structure linear_ordered_add_comm_group (α : Type u) :
Type u

A linearly ordered additive commutative group is an additive commutative group with a linear order in which addition is monotone.

Instances of this typeclass
Instances of other typeclasses for linear_ordered_add_comm_group
  • linear_ordered_add_comm_group.has_sizeof_inst
source
@[instance]
def linear_ordered_add_comm_group_with_top.to_sub_neg_monoid (α : Type u_1) [self : linear_ordered_add_comm_group_with_top α] :
sub_neg_monoid α
source
@[class]
structure linear_ordered_add_comm_group_with_top (α : Type u_1) :
Type u_1

A linearly ordered commutative monoid with an additively absorbing ⊤ element. Instances should include number systems with an infinite element adjoined.`

Instances of this typeclass
Instances of other typeclasses for linear_ordered_add_comm_group_with_top
  • linear_ordered_add_comm_group_with_top.has_sizeof_inst
source
@[instance]
def linear_ordered_add_comm_group_with_top.to_linear_ordered_add_comm_monoid_with_top (α : Type u_1) [self : linear_ordered_add_comm_group_with_top α] :
linear_ordered_add_comm_monoid_with_top α
source
@[instance]
def linear_ordered_add_comm_group_with_top.to_nontrivial (α : Type u_1) [self : linear_ordered_add_comm_group_with_top α] :
nontrivial α
source
@[class]
structure linear_ordered_comm_group (α : Type u) :
Type u

A linearly ordered commutative group is a commutative group with a linear order in which multiplication is monotone.

Instances of this typeclass
Instances of other typeclasses for linear_ordered_comm_group
  • linear_ordered_comm_group.has_sizeof_inst
source
@[instance]
def linear_ordered_comm_group.to_ordered_comm_group (α : Type u) [self : linear_ordered_comm_group α] :
ordered_comm_group α
source
@[instance]
def linear_ordered_comm_group.to_linear_order (α : Type u) [self : linear_ordered_comm_group α] :
linear_order α
source
theorem linear_ordered_comm_group.mul_lt_mul_left' {α : Type u} [linear_ordered_comm_group α] (a b : α) (h : a < b) (c : α) :
c * a < c * b
source
theorem linear_ordered_add_comm_group.add_lt_add_left {α : Type u} [linear_ordered_add_comm_group α] (a b : α) (h : a < b) (c : α) :
c + a < c + b
source
theorem eq_zero_of_neg_eq {α : Type u} [linear_ordered_add_comm_group α] {a : α} (h : -a = a) :
a = 0
source
theorem eq_one_of_inv_eq' {α : Type u} [linear_ordered_comm_group α] {a : α} (h : a⁻¹ = a) :
a = 1
source
theorem exists_one_lt' {α : Type u} [linear_ordered_comm_group α] [nontrivial α] :
∃ (a : α), 1 < a
source
theorem exists_zero_lt {α : Type u} [linear_ordered_add_comm_group α] [nontrivial α] :
∃ (a : α), 0 < a
source
@[protected, instance]
def linear_ordered_add_comm_group.to_no_max_order {α : Type u} [linear_ordered_add_comm_group α] [nontrivial α] :
no_max_order α
source
@[protected, instance]
def linear_ordered_comm_group.to_no_max_order {α : Type u} [linear_ordered_comm_group α] [nontrivial α] :
no_max_order α
source
@[protected, instance]
def linear_ordered_comm_group.to_no_min_order {α : Type u} [linear_ordered_comm_group α] [nontrivial α] :
no_min_order α
source
@[protected, instance]
def linear_ordered_add_comm_group.to_no_min_order {α : Type u} [linear_ordered_add_comm_group α] [nontrivial α] :
no_min_order α
source
@[protected, instance]
def linear_ordered_add_comm_group.to_linear_ordered_cancel_add_comm_monoid {α : Type u} [linear_ordered_add_comm_group α] :
linear_ordered_cancel_add_comm_monoid α
Equations
source
@[protected, instance]
def linear_ordered_comm_group.to_linear_ordered_cancel_comm_monoid {α : Type u} [linear_ordered_comm_group α] :
linear_ordered_cancel_comm_monoid α
Equations
source
@[nolint]
structure add_comm_group.positive_cone (α : Type u_1) [add_comm_group α] :
Type u_1

A collection of elements in an add_comm_group designated as "non-negative". This is useful for constructing an ordered_add_commm_group by choosing a positive cone in an exisiting add_comm_group.

Instances for add_comm_group.positive_cone
  • add_comm_group.positive_cone.has_sizeof_inst
source
def add_comm_group.total_positive_cone.to_positive_cone {α : Type u_1} [add_comm_group α] (self : add_comm_group.total_positive_cone α) :
add_comm_group.positive_cone α

Forget that a total_positive_cone is total.

source
@[nolint]
structure add_comm_group.total_positive_cone (α : Type u_1) [add_comm_group α] :
Type u_1

A positive cone in an add_comm_group induces a linear order if for every a, either a or -a is non-negative.

Instances for add_comm_group.total_positive_cone
  • add_comm_group.total_positive_cone.has_sizeof_inst
source
def ordered_add_comm_group.mk_of_positive_cone {α : Type u_1} [add_comm_group α] (C : add_comm_group.positive_cone α) :
ordered_add_comm_group α

Construct an ordered_add_comm_group by designating a positive cone in an existing add_comm_group.

Equations
source
def linear_ordered_add_comm_group.mk_of_positive_cone {α : Type u_1} [add_comm_group α] (C : add_comm_group.total_positive_cone α) :
linear_ordered_add_comm_group α

Construct a linear_ordered_add_comm_group by designating a positive cone in an existing add_comm_group such that for every a, either a or -a is non-negative.

Equations
source
theorem neg_le_neg {α : Type u} [ordered_add_comm_group α] {a b : α} :
a ≤ b → -b ≤ -a
source
theorem inv_le_inv' {α : Type u} [ordered_comm_group α] {a b : α} :
a ≤ b → b⁻¹ ≤ a⁻¹
source
theorem neg_lt_neg {α : Type u} [ordered_add_comm_group α] {a b : α} :
a < b → -b < -a
source
theorem inv_lt_inv' {α : Type u} [ordered_comm_group α] {a b : α} :
a < b → b⁻¹ < a⁻¹
source
theorem inv_lt_one_of_one_lt {α : Type u} [ordered_comm_group α] {a : α} :
1 < a → a⁻¹ < 1
source
theorem neg_neg_of_pos {α : Type u} [ordered_add_comm_group α] {a : α} :
0 < a → -a < 0
source
theorem inv_le_one_of_one_le {α : Type u} [ordered_comm_group α] {a : α} :
1 ≤ a → a⁻¹ ≤ 1
source
theorem neg_nonpos_of_nonneg {α : Type u} [ordered_add_comm_group α] {a : α} :
0 ≤ a → -a ≤ 0
source
theorem one_le_inv_of_le_one {α : Type u} [ordered_comm_group α] {a : α} :
a ≤ 1 → 1 ≤ a⁻¹
source
theorem neg_nonneg_of_nonpos {α : Type u} [ordered_add_comm_group α] {a : α} :
a ≤ 0 → 0 ≤ -a
source
theorem monotone.neg {α : Type u} {β : Type u_1} [add_group α] [preorder α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] [preorder β] {f : β → α} (hf : monotone f) :
antitone (λ (x : β), -f x)
source
theorem monotone.inv {α : Type u} {β : Type u_1} [group α] [preorder α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] [preorder β] {f : β → α} (hf : monotone f) :
antitone (λ (x : β), (f x)⁻¹)
source
theorem antitone.inv {α : Type u} {β : Type u_1} [group α] [preorder α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] [preorder β] {f : β → α} (hf : antitone f) :
monotone (λ (x : β), (f x)⁻¹)
source
theorem antitone.neg {α : Type u} {β : Type u_1} [add_group α] [preorder α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] [preorder β] {f : β → α} (hf : antitone f) :
monotone (λ (x : β), -f x)
source
theorem monotone_on.inv {α : Type u} {β : Type u_1} [group α] [preorder α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] [preorder β] {f : β → α} {s : set β} (hf : monotone_on f s) :
antitone_on (λ (x : β), (f x)⁻¹) s
source
theorem monotone_on.neg {α : Type u} {β : Type u_1} [add_group α] [preorder α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] [preorder β] {f : β → α} {s : set β} (hf : monotone_on f s) :
antitone_on (λ (x : β), -f x) s
source
theorem antitone_on.neg {α : Type u} {β : Type u_1} [add_group α] [preorder α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] [preorder β] {f : β → α} {s : set β} (hf : antitone_on f s) :
monotone_on (λ (x : β), -f x) s
source
theorem antitone_on.inv {α : Type u} {β : Type u_1} [group α] [preorder α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] [preorder β] {f : β → α} {s : set β} (hf : antitone_on f s) :
monotone_on (λ (x : β), (f x)⁻¹) s
source
theorem strict_mono.inv {α : Type u} {β : Type u_1} [group α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] [preorder β] {f : β → α} (hf : strict_mono f) :
strict_anti (λ (x : β), (f x)⁻¹)
source
theorem strict_mono.neg {α : Type u} {β : Type u_1} [add_group α] [preorder α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] [preorder β] {f : β → α} (hf : strict_mono f) :
strict_anti (λ (x : β), -f x)
source
theorem strict_anti.neg {α : Type u} {β : Type u_1} [add_group α] [preorder α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] [preorder β] {f : β → α} (hf : strict_anti f) :
strict_mono (λ (x : β), -f x)
source
theorem strict_anti.inv {α : Type u} {β : Type u_1} [group α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] [preorder β] {f : β → α} (hf : strict_anti f) :
strict_mono (λ (x : β), (f x)⁻¹)
source
theorem strict_mono_on.neg {α : Type u} {β : Type u_1} [add_group α] [preorder α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] [preorder β] {f : β → α} {s : set β} (hf : strict_mono_on f s) :
strict_anti_on (λ (x : β), -f x) s
source
theorem strict_mono_on.inv {α : Type u} {β : Type u_1} [group α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] [preorder β] {f : β → α} {s : set β} (hf : strict_mono_on f s) :
strict_anti_on (λ (x : β), (f x)⁻¹) s
source
theorem strict_anti_on.inv {α : Type u} {β : Type u_1} [group α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] [preorder β] {f : β → α} {s : set β} (hf : strict_anti_on f s) :
strict_mono_on (λ (x : β), (f x)⁻¹) s
source
theorem strict_anti_on.neg {α : Type u} {β : Type u_1} [add_group α] [preorder α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] [preorder β] {f : β → α} {s : set β} (hf : strict_anti_on f s) :
strict_mono_on (λ (x : β), -f x) s