mathlib documentation

algebra.order.ring.defs

Ordered rings and semirings #

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

This file develops the basics of ordered (semi)rings.

Each typeclass here comprises

For short,

Typeclasses #

Hierarchy #

The hardest part of proving order lemmas might be to figure out the correct generality and its corresponding typeclass. Here's an attempt at demystifying it. For each typeclass, we list its immediate predecessors and what conditions are added to each of them.

Note that order_dual does not satisfy any of the ordered ring typeclasses due to the zero_le_one field.

theorem add_one_le_two_mul {α : Type u} [has_le α] [semiring α] [covariant_class α α has_add.add has_le.le] {a : α} (a1 : 1 a) :
a + 1 2 * a
@[instance]
@[class]
structure ordered_semiring (α : Type u) :

An ordered_semiring is a semiring with a partial order such that addition is monotone and multiplication by a nonnegative number is monotone.

Instances of this typeclass
Instances of other typeclasses for ordered_semiring
  • ordered_semiring.has_sizeof_inst
@[class]
structure ordered_comm_semiring (α : Type u) :

An ordered_comm_semiring is a commutative semiring with a partial order such that addition is monotone and multiplication by a nonnegative number is monotone.

Instances of this typeclass
Instances of other typeclasses for ordered_comm_semiring
  • ordered_comm_semiring.has_sizeof_inst
@[class]
structure ordered_ring (α : Type u) :

An ordered_ring is a ring with a partial order such that addition is monotone and multiplication by a nonnegative number is monotone.

Instances of this typeclass
Instances of other typeclasses for ordered_ring
  • ordered_ring.has_sizeof_inst
@[instance]
def ordered_ring.to_ring (α : Type u) [self : ordered_ring α] :
ring α
@[instance]
@[instance]
@[class]
structure ordered_comm_ring (α : Type u) :

An ordered_comm_ring is a commutative ring with a partial order such that addition is monotone and multiplication by a nonnegative number is monotone.

Instances of this typeclass
Instances of other typeclasses for ordered_comm_ring
  • ordered_comm_ring.has_sizeof_inst
@[class]
structure strict_ordered_semiring (α : Type u) :

A strict_ordered_semiring is a nontrivial semiring with a partial order such that addition is strictly monotone and multiplication by a positive number is strictly monotone.

Instances of this typeclass
Instances of other typeclasses for strict_ordered_semiring
  • strict_ordered_semiring.has_sizeof_inst
@[class]
structure strict_ordered_comm_semiring (α : Type u) :

A strict_ordered_comm_semiring is a commutative semiring with a partial order such that addition is strictly monotone and multiplication by a positive number is strictly monotone.

Instances of this typeclass
Instances of other typeclasses for strict_ordered_comm_semiring
  • strict_ordered_comm_semiring.has_sizeof_inst
@[class]
structure strict_ordered_ring (α : Type u) :

A strict_ordered_ring is a ring with a partial order such that addition is strictly monotone and multiplication by a positive number is strictly monotone.

Instances of this typeclass
Instances of other typeclasses for strict_ordered_ring
  • strict_ordered_ring.has_sizeof_inst
@[instance]
@[instance]
def strict_ordered_ring.to_ring (α : Type u) [self : strict_ordered_ring α] :
ring α
@[class]
structure strict_ordered_comm_ring (α : Type u_2) :
Type u_2

A strict_ordered_comm_ring is a commutative ring with a partial order such that addition is strictly monotone and multiplication by a positive number is strictly monotone.

Instances of this typeclass
Instances of other typeclasses for strict_ordered_comm_ring
  • strict_ordered_comm_ring.has_sizeof_inst
@[class]
structure linear_ordered_semiring (α : Type u) :

A linear_ordered_semiring is a nontrivial semiring with a linear order such that addition is monotone and multiplication by a positive number is strictly monotone.

Instances of this typeclass
Instances of other typeclasses for linear_ordered_semiring
  • linear_ordered_semiring.has_sizeof_inst
@[class]
structure linear_ordered_comm_semiring (α : Type u_2) :
Type u_2

A linear_ordered_comm_semiring is a nontrivial commutative semiring with a linear order such that addition is monotone and multiplication by a positive number is strictly monotone.

Instances of this typeclass
Instances of other typeclasses for linear_ordered_comm_semiring
  • linear_ordered_comm_semiring.has_sizeof_inst
@[class]
structure linear_ordered_ring (α : Type u) :

A linear_ordered_ring is a ring with a linear order such that addition is monotone and multiplication by a positive number is strictly monotone.

Instances of this typeclass
Instances of other typeclasses for linear_ordered_ring
  • linear_ordered_ring.has_sizeof_inst
@[class]
structure linear_ordered_comm_ring (α : Type u) :

A linear_ordered_comm_ring is a commutative ring with a linear order such that addition is monotone and multiplication by a positive number is strictly monotone.

Instances of this typeclass
Instances of other typeclasses for linear_ordered_comm_ring
  • linear_ordered_comm_ring.has_sizeof_inst
@[protected, instance]
@[protected, instance]
theorem bit1_mono {α : Type u} [ordered_semiring α] :
@[simp]
theorem pow_nonneg {α : Type u} [ordered_semiring α] {a : α} (H : 0 a) (n : ) :
0 a ^ n
theorem add_le_mul_two_add {α : Type u} [ordered_semiring α] {a b : α} (a2 : 2 a) (b0 : 0 b) :
a + (2 + b) a * (2 + b)
theorem one_le_mul_of_one_le_of_one_le {α : Type u} [ordered_semiring α] {a b : α} (ha : 1 a) (hb : 1 b) :
1 a * b
theorem monotone_mul_left_of_nonneg {α : Type u} [ordered_semiring α] {a : α} (ha : 0 a) :
monotone (λ (x : α), a * x)
theorem monotone_mul_right_of_nonneg {α : Type u} [ordered_semiring α] {a : α} (ha : 0 a) :
monotone (λ (x : α), x * a)
theorem monotone.mul_const {α : Type u} {β : Type u_1} [ordered_semiring α] {a : α} [preorder β] {f : β α} (hf : monotone f) (ha : 0 a) :
monotone (λ (x : β), f x * a)
theorem monotone.const_mul {α : Type u} {β : Type u_1} [ordered_semiring α] {a : α} [preorder β] {f : β α} (hf : monotone f) (ha : 0 a) :
monotone (λ (x : β), a * f x)
theorem antitone.mul_const {α : Type u} {β : Type u_1} [ordered_semiring α] {a : α} [preorder β] {f : β α} (hf : antitone f) (ha : 0 a) :
antitone (λ (x : β), f x * a)
theorem antitone.const_mul {α : Type u} {β : Type u_1} [ordered_semiring α] {a : α} [preorder β] {f : β α} (hf : antitone f) (ha : 0 a) :
antitone (λ (x : β), a * f x)
theorem monotone.mul {α : Type u} {β : Type u_1} [ordered_semiring α] [preorder β] {f g : β α} (hf : monotone f) (hg : monotone g) (hf₀ : (x : β), 0 f x) (hg₀ : (x : β), 0 g x) :
monotone (f * g)
theorem bit1_pos {α : Type u} [ordered_semiring α] {a : α} [nontrivial α] (h : 0 a) :
0 < bit1 a
theorem bit1_pos' {α : Type u} [ordered_semiring α] {a : α} (h : 0 < a) :
0 < bit1 a
theorem mul_le_one {α : Type u} [ordered_semiring α] {a b : α} (ha : a 1) (hb' : 0 b) (hb : b 1) :
a * b 1
theorem one_lt_mul_of_le_of_lt {α : Type u} [ordered_semiring α] {a b : α} (ha : 1 a) (hb : 1 < b) :
1 < a * b
theorem one_lt_mul_of_lt_of_le {α : Type u} [ordered_semiring α] {a b : α} (ha : 1 < a) (hb : 1 b) :
1 < a * b
theorem one_lt_mul {α : Type u} [ordered_semiring α] {a b : α} (ha : 1 a) (hb : 1 < b) :
1 < a * b

Alias of one_lt_mul_of_le_of_lt.

theorem mul_lt_one_of_nonneg_of_lt_one_left {α : Type u} [ordered_semiring α] {a b : α} (ha₀ : 0 a) (ha : a < 1) (hb : b 1) :
a * b < 1
theorem mul_lt_one_of_nonneg_of_lt_one_right {α : Type u} [ordered_semiring α] {a b : α} (ha : a 1) (hb₀ : 0 b) (hb : b < 1) :
a * b < 1
theorem mul_le_mul_of_nonpos_left {α : Type u} [ordered_ring α] {a b c : α} (h : b a) (hc : c 0) :
c * a c * b
theorem mul_le_mul_of_nonpos_right {α : Type u} [ordered_ring α] {a b c : α} (h : b a) (hc : c 0) :
a * c b * c
theorem mul_nonneg_of_nonpos_of_nonpos {α : Type u} [ordered_ring α] {a b : α} (ha : a 0) (hb : b 0) :
0 a * b
theorem mul_le_mul_of_nonneg_of_nonpos {α : Type u} [ordered_ring α] {a b c d : α} (hca : c a) (hbd : b d) (hc : 0 c) (hb : b 0) :
a * b c * d
theorem mul_le_mul_of_nonneg_of_nonpos' {α : Type u} [ordered_ring α] {a b c d : α} (hca : c a) (hbd : b d) (ha : 0 a) (hd : d 0) :
a * b c * d
theorem mul_le_mul_of_nonpos_of_nonneg {α : Type u} [ordered_ring α] {a b c d : α} (hac : a c) (hdb : d b) (hc : c 0) (hb : 0 b) :
a * b c * d
theorem mul_le_mul_of_nonpos_of_nonneg' {α : Type u} [ordered_ring α] {a b c d : α} (hca : c a) (hbd : b d) (ha : 0 a) (hd : d 0) :
a * b c * d
theorem mul_le_mul_of_nonpos_of_nonpos {α : Type u} [ordered_ring α] {a b c d : α} (hca : c a) (hdb : d b) (hc : c 0) (hb : b 0) :
a * b c * d
theorem mul_le_mul_of_nonpos_of_nonpos' {α : Type u} [ordered_ring α] {a b c d : α} (hca : c a) (hdb : d b) (ha : a 0) (hd : d 0) :
a * b c * d
theorem antitone_mul_left {α : Type u} [ordered_ring α] {a : α} (ha : a 0) :
theorem antitone_mul_right {α : Type u} [ordered_ring α] {a : α} (ha : a 0) :
antitone (λ (x : α), x * a)
theorem monotone.const_mul_of_nonpos {α : Type u} {β : Type u_1} [ordered_ring α] {a : α} [preorder β] {f : β α} (hf : monotone f) (ha : a 0) :
antitone (λ (x : β), a * f x)
theorem monotone.mul_const_of_nonpos {α : Type u} {β : Type u_1} [ordered_ring α] {a : α} [preorder β] {f : β α} (hf : monotone f) (ha : a 0) :
antitone (λ (x : β), f x * a)
theorem antitone.const_mul_of_nonpos {α : Type u} {β : Type u_1} [ordered_ring α] {a : α} [preorder β] {f : β α} (hf : antitone f) (ha : a 0) :
monotone (λ (x : β), a * f x)
theorem antitone.mul_const_of_nonpos {α : Type u} {β : Type u_1} [ordered_ring α] {a : α} [preorder β] {f : β α} (hf : antitone f) (ha : a 0) :
monotone (λ (x : β), f x * a)
theorem antitone.mul_monotone {α : Type u} {β : Type u_1} [ordered_ring α] [preorder β] {f g : β α} (hf : antitone f) (hg : monotone g) (hf₀ : (x : β), f x 0) (hg₀ : (x : β), 0 g x) :
antitone (f * g)
theorem monotone.mul_antitone {α : Type u} {β : Type u_1} [ordered_ring α] [preorder β] {f g : β α} (hf : monotone f) (hg : antitone g) (hf₀ : (x : β), 0 f x) (hg₀ : (x : β), g x 0) :
antitone (f * g)
theorem antitone.mul {α : Type u} {β : Type u_1} [ordered_ring α] [preorder β] {f g : β α} (hf : antitone f) (hg : antitone g) (hf₀ : (x : β), f x 0) (hg₀ : (x : β), g x 0) :
monotone (f * g)
theorem le_iff_exists_nonneg_add {α : Type u} [ordered_ring α] (a b : α) :
a b (c : α) (H : c 0), b = a + c
theorem mul_lt_mul {α : Type u} [strict_ordered_semiring α] {a b c d : α} (hac : a < c) (hbd : b d) (hb : 0 < b) (hc : 0 c) :
a * b < c * d
theorem mul_lt_mul' {α : Type u} [strict_ordered_semiring α] {a b c d : α} (hac : a c) (hbd : b < d) (hb : 0 b) (hc : 0 < c) :
a * b < c * d
@[simp]
theorem pow_pos {α : Type u} [strict_ordered_semiring α] {a : α} (H : 0 < a) (n : ) :
0 < a ^ n
theorem mul_self_lt_mul_self {α : Type u} [strict_ordered_semiring α] {a b : α} (h1 : 0 a) (h2 : a < b) :
a * a < b * b
theorem strict_mono_on_mul_self {α : Type u} [strict_ordered_semiring α] :
strict_mono_on (λ (x : α), x * x) {x : α | 0 x}
@[protected]
theorem decidable.mul_lt_mul'' {α : Type u} [strict_ordered_semiring α] {a b c d : α} [decidable_rel has_le.le] (h1 : a < c) (h2 : b < d) (h3 : 0 a) (h4 : 0 b) :
a * b < c * d
theorem mul_lt_mul'' {α : Type u} [strict_ordered_semiring α] {a b c d : α} :
a < c b < d 0 a 0 b a * b < c * d
theorem lt_mul_left {α : Type u} [strict_ordered_semiring α] {a b : α} (hn : 0 < a) (hm : 1 < b) :
a < b * a
theorem lt_mul_right {α : Type u} [strict_ordered_semiring α] {a b : α} (hn : 0 < a) (hm : 1 < b) :
a < a * b
theorem lt_mul_self {α : Type u} [strict_ordered_semiring α] {a : α} (hn : 1 < a) :
a < a * a
theorem strict_mono_mul_left_of_pos {α : Type u} [strict_ordered_semiring α] {a : α} (ha : 0 < a) :
strict_mono (λ (x : α), a * x)
theorem strict_mono_mul_right_of_pos {α : Type u} [strict_ordered_semiring α] {a : α} (ha : 0 < a) :
strict_mono (λ (x : α), x * a)
theorem strict_mono.mul_const {α : Type u} {β : Type u_1} [strict_ordered_semiring α] {a : α} [preorder β] {f : β α} (hf : strict_mono f) (ha : 0 < a) :
strict_mono (λ (x : β), f x * a)
theorem strict_mono.const_mul {α : Type u} {β : Type u_1} [strict_ordered_semiring α] {a : α} [preorder β] {f : β α} (hf : strict_mono f) (ha : 0 < a) :
strict_mono (λ (x : β), a * f x)
theorem strict_anti.mul_const {α : Type u} {β : Type u_1} [strict_ordered_semiring α] {a : α} [preorder β] {f : β α} (hf : strict_anti f) (ha : 0 < a) :
strict_anti (λ (x : β), f x * a)
theorem strict_anti.const_mul {α : Type u} {β : Type u_1} [strict_ordered_semiring α] {a : α} [preorder β] {f : β α} (hf : strict_anti f) (ha : 0 < a) :
strict_anti (λ (x : β), a * f x)
theorem strict_mono.mul_monotone {α : Type u} {β : Type u_1} [strict_ordered_semiring α] [preorder β] {f g : β α} (hf : strict_mono f) (hg : monotone g) (hf₀ : (x : β), 0 f x) (hg₀ : (x : β), 0 < g x) :
theorem monotone.mul_strict_mono {α : Type u} {β : Type u_1} [strict_ordered_semiring α] [preorder β] {f g : β α} (hf : monotone f) (hg : strict_mono g) (hf₀ : (x : β), 0 < f x) (hg₀ : (x : β), 0 g x) :
theorem strict_mono.mul {α : Type u} {β : Type u_1} [strict_ordered_semiring α] [preorder β] {f g : β α} (hf : strict_mono f) (hg : strict_mono g) (hf₀ : (x : β), 0 f x) (hg₀ : (x : β), 0 g x) :
theorem lt_two_mul_self {α : Type u} [strict_ordered_semiring α] {a : α} (ha : 0 < a) :
a < 2 * a
theorem mul_lt_mul_of_neg_left {α : Type u} [strict_ordered_ring α] {a b c : α} (h : b < a) (hc : c < 0) :
c * a < c * b
theorem mul_lt_mul_of_neg_right {α : Type u} [strict_ordered_ring α] {a b c : α} (h : b < a) (hc : c < 0) :
a * c < b * c
theorem mul_pos_of_neg_of_neg {α : Type u} [strict_ordered_ring α] {a b : α} (ha : a < 0) (hb : b < 0) :
0 < a * b
theorem strict_anti_mul_left {α : Type u} [strict_ordered_ring α] {a : α} (ha : a < 0) :
theorem strict_anti_mul_right {α : Type u} [strict_ordered_ring α] {a : α} (ha : a < 0) :
strict_anti (λ (x : α), x * a)
theorem strict_mono.const_mul_of_neg {α : Type u} {β : Type u_1} [strict_ordered_ring α] {a : α} [preorder β] {f : β α} (hf : strict_mono f) (ha : a < 0) :
strict_anti (λ (x : β), a * f x)
theorem strict_mono.mul_const_of_neg {α : Type u} {β : Type u_1} [strict_ordered_ring α] {a : α} [preorder β] {f : β α} (hf : strict_mono f) (ha : a < 0) :
strict_anti (λ (x : β), f x * a)
theorem strict_anti.const_mul_of_neg {α : Type u} {β : Type u_1} [strict_ordered_ring α] {a : α} [preorder β] {f : β α} (hf : strict_anti f) (ha : a < 0) :
strict_mono (λ (x : β), a * f x)
theorem strict_anti.mul_const_of_neg {α : Type u} {β : Type u_1} [strict_ordered_ring α] {a : α} [preorder β] {f : β α} (hf : strict_anti f) (ha : a < 0) :
strict_mono (λ (x : β), f x * a)
theorem nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nnonneg {α : Type u} [linear_ordered_semiring α] {a b : α} (hab : 0 a * b) :
0 a 0 b a 0 b 0
theorem nonneg_of_mul_nonneg_left {α : Type u} [linear_ordered_semiring α] {a b : α} (h : 0 a * b) (hb : 0 < b) :
0 a
theorem nonneg_of_mul_nonneg_right {α : Type u} [linear_ordered_semiring α] {a b : α} (h : 0 a * b) (ha : 0 < a) :
0 b
theorem neg_of_mul_neg_left {α : Type u} [linear_ordered_semiring α] {a b : α} (h : a * b < 0) (hb : 0 b) :
a < 0
theorem neg_of_mul_neg_right {α : Type u} [linear_ordered_semiring α] {a b : α} (h : a * b < 0) (ha : 0 a) :
b < 0
theorem nonpos_of_mul_nonpos_left {α : Type u} [linear_ordered_semiring α] {a b : α} (h : a * b 0) (hb : 0 < b) :
a 0
theorem nonpos_of_mul_nonpos_right {α : Type u} [linear_ordered_semiring α] {a b : α} (h : a * b 0) (ha : 0 < a) :
b 0
@[simp]
theorem zero_le_mul_left {α : Type u} [linear_ordered_semiring α] {b c : α} (h : 0 < c) :
0 c * b 0 b
@[simp]
theorem zero_le_mul_right {α : Type u} [linear_ordered_semiring α] {b c : α} (h : 0 < c) :
0 b * c 0 b
theorem add_le_mul_of_left_le_right {α : Type u} [linear_ordered_semiring α] {a b : α} (a2 : 2 a) (ab : a b) :
a + b a * b
theorem add_le_mul_of_right_le_left {α : Type u} [linear_ordered_semiring α] {a b : α} (b2 : 2 b) (ba : b a) :
a + b a * b
theorem add_le_mul {α : Type u} [linear_ordered_semiring α] {a b : α} (a2 : 2 a) (b2 : 2 b) :
a + b a * b
theorem add_le_mul' {α : Type u} [linear_ordered_semiring α] {a b : α} (a2 : 2 a) (b2 : 2 b) :
a + b b * a
@[simp]
theorem bit0_le_bit0 {α : Type u} [linear_ordered_semiring α] {a b : α} :
bit0 a bit0 b a b
@[simp]
theorem bit0_lt_bit0 {α : Type u} [linear_ordered_semiring α] {a b : α} :
bit0 a < bit0 b a < b
@[simp]
theorem bit1_le_bit1 {α : Type u} [linear_ordered_semiring α] {a b : α} :
bit1 a bit1 b a b
@[simp]
theorem bit1_lt_bit1 {α : Type u} [linear_ordered_semiring α] {a b : α} :
bit1 a < bit1 b a < b
@[simp]
theorem one_le_bit1 {α : Type u} [linear_ordered_semiring α] {a : α} :
1 bit1 a 0 a
@[simp]
theorem one_lt_bit1 {α : Type u} [linear_ordered_semiring α] {a : α} :
1 < bit1 a 0 < a
@[simp]
theorem zero_le_bit0 {α : Type u} [linear_ordered_semiring α] {a : α} :
0 bit0 a 0 a
@[simp]
theorem zero_lt_bit0 {α : Type u} [linear_ordered_semiring α] {a : α} :
0 < bit0 a 0 < a
theorem mul_nonneg_iff_right_nonneg_of_pos {α : Type u} [linear_ordered_semiring α] {a b : α} (ha : 0 < a) :
0 a * b 0 b
theorem mul_nonneg_iff_left_nonneg_of_pos {α : Type u} [linear_ordered_semiring α] {a b : α} (hb : 0 < b) :
0 a * b 0 a
theorem nonpos_of_mul_nonneg_left {α : Type u} [linear_ordered_semiring α] {a b : α} (h : 0 a * b) (hb : b < 0) :
a 0
theorem nonpos_of_mul_nonneg_right {α : Type u} [linear_ordered_semiring α] {a b : α} (h : 0 a * b) (ha : a < 0) :
b 0
@[simp]
theorem units.inv_pos {α : Type u} [linear_ordered_semiring α] {u : αˣ} :
@[simp]
theorem units.inv_neg {α : Type u} [linear_ordered_semiring α] {u : αˣ} :
theorem cmp_mul_pos_left {α : Type u} [linear_ordered_semiring α] {a : α} (ha : 0 < a) (b c : α) :
cmp (a * b) (a * c) = cmp b c
theorem cmp_mul_pos_right {α : Type u} [linear_ordered_semiring α] {a : α} (ha : 0 < a) (b c : α) :
cmp (b * a) (c * a) = cmp b c
theorem mul_max_of_nonneg {α : Type u} [linear_ordered_semiring α] {a : α} (b c : α) (ha : 0 a) :
theorem mul_min_of_nonneg {α : Type u} [linear_ordered_semiring α] {a : α} (b c : α) (ha : 0 a) :
theorem max_mul_of_nonneg {α : Type u} [linear_ordered_semiring α] {c : α} (a b : α) (hc : 0 c) :
theorem min_mul_of_nonneg {α : Type u} [linear_ordered_semiring α] {c : α} (a b : α) (hc : 0 c) :
theorem le_of_mul_le_of_one_le {α : Type u} [linear_ordered_semiring α] {a b c : α} (h : a * c b) (hb : 0 b) (hc : 1 c) :
a b
theorem nonneg_le_nonneg_of_sq_le_sq {α : Type u} [linear_ordered_semiring α] {a b : α} (hb : 0 b) (h : a * a b * b) :
a b
theorem mul_self_le_mul_self_iff {α : Type u} [linear_ordered_semiring α] {a b : α} (h1 : 0 a) (h2 : 0 b) :
a b a * a b * b
theorem mul_self_lt_mul_self_iff {α : Type u} [linear_ordered_semiring α] {a b : α} (h1 : 0 a) (h2 : 0 b) :
a < b a * a < b * b
theorem mul_self_inj {α : Type u} [linear_ordered_semiring α] {a b : α} (h1 : 0 a) (h2 : 0 b) :
a * a = b * b a = b
@[protected, instance]
theorem mul_pos_iff {α : Type u} [linear_ordered_ring α] {a b : α} :
0 < a * b 0 < a 0 < b a < 0 b < 0
theorem mul_neg_iff {α : Type u} [linear_ordered_ring α] {a b : α} :
a * b < 0 0 < a b < 0 a < 0 0 < b
theorem mul_nonneg_iff {α : Type u} [linear_ordered_ring α] {a b : α} :
0 a * b 0 a 0 b a 0 b 0
theorem mul_nonneg_of_three {α : Type u} [linear_ordered_ring α] (a b c : α) :
0 a * b 0 b * c 0 c * a

Out of three elements of a linear_ordered_ring, two must have the same sign.

theorem mul_nonpos_iff {α : Type u} [linear_ordered_ring α] {a b : α} :
a * b 0 0 a b 0 a 0 0 b
theorem mul_self_nonneg {α : Type u} [linear_ordered_ring α] (a : α) :
0 a * a
@[simp]
theorem neg_le_self_iff {α : Type u} [linear_ordered_ring α] {a : α} :
-a a 0 a
@[simp]
theorem neg_lt_self_iff {α : Type u} [linear_ordered_ring α] {a : α} :
-a < a 0 < a
@[simp]
theorem le_neg_self_iff {α : Type u} [linear_ordered_ring α] {a : α} :
a -a a 0
@[simp]
theorem lt_neg_self_iff {α : Type u} [linear_ordered_ring α] {a : α} :
a < -a a < 0
theorem neg_one_lt_zero {α : Type u} [linear_ordered_ring α] :
-1 < 0
@[simp]
theorem mul_le_mul_left_of_neg {α : Type u} [linear_ordered_ring α] {a b c : α} (h : c < 0) :
c * a c * b b a
@[simp]
theorem mul_le_mul_right_of_neg {α : Type u} [linear_ordered_ring α] {a b c : α} (h : c < 0) :
a * c b * c b a
@[simp]
theorem mul_lt_mul_left_of_neg {α : Type u} [linear_ordered_ring α] {a b c : α} (h : c < 0) :
c * a < c * b b < a
@[simp]
theorem mul_lt_mul_right_of_neg {α : Type u} [linear_ordered_ring α] {a b c : α} (h : c < 0) :
a * c < b * c b < a
theorem lt_of_mul_lt_mul_of_nonpos_left {α : Type u} [linear_ordered_ring α] {a b c : α} (h : c * a < c * b) (hc : c 0) :
b < a
theorem lt_of_mul_lt_mul_of_nonpos_right {α : Type u} [linear_ordered_ring α] {a b c : α} (h : a * c < b * c) (hc : c 0) :
b < a
theorem cmp_mul_neg_left {α : Type u} [linear_ordered_ring α] {a : α} (ha : a < 0) (b c : α) :
cmp (a * b) (a * c) = cmp c b
theorem cmp_mul_neg_right {α : Type u} [linear_ordered_ring α] {a : α} (ha : a < 0) (b c : α) :
cmp (b * a) (c * a) = cmp c b
theorem sub_one_lt {α : Type u} [linear_ordered_ring α] (a : α) :
a - 1 < a
@[simp]
theorem mul_self_pos {α : Type u} [linear_ordered_ring α] {a : α} :
0 < a * a a 0
theorem mul_self_le_mul_self_of_le_of_neg_le {α : Type u} [linear_ordered_ring α] {x y : α} (h₁ : x y) (h₂ : -x y) :
x * x y * y
theorem nonneg_of_mul_nonpos_left {α : Type u} [linear_ordered_ring α] {a b : α} (h : a * b 0) (hb : b < 0) :
0 a
theorem nonneg_of_mul_nonpos_right {α : Type u} [linear_ordered_ring α] {a b : α} (h : a * b 0) (ha : a < 0) :
0 b
theorem pos_of_mul_neg_left {α : Type u} [linear_ordered_ring α] {a b : α} (h : a * b < 0) (hb : b 0) :
0 < a
theorem pos_of_mul_neg_right {α : Type u} [linear_ordered_ring α] {a b : α} (h : a * b < 0) (ha : a 0) :
0 < b
theorem neg_iff_pos_of_mul_neg {α : Type u} [linear_ordered_ring α] {a b : α} (hab : a * b < 0) :
a < 0 0 < b
theorem pos_iff_neg_of_mul_neg {α : Type u} [linear_ordered_ring α] {a b : α} (hab : a * b < 0) :
0 < a b < 0
theorem mul_self_add_mul_self_eq_zero {α : Type u} [linear_ordered_ring α] {x y : α} :
x * x + y * y = 0 x = 0 y = 0

The sum of two squares is zero iff both elements are zero.

theorem eq_zero_of_mul_self_add_mul_self_eq_zero {α : Type u} [linear_ordered_ring α] {a b : α} (h : a * a + b * b = 0) :
a = 0
theorem max_mul_mul_le_max_mul_max {α : Type u} [linear_ordered_comm_ring α] {a d : α} (b c : α) (ha : 0 a) (hd : 0 d) :