# mathlibdocumentation

algebra.ordered_ring

# Ordered rings and semirings #

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

Each typeclass here comprises

• an algebraic class (`semiring`, `comm_semiring`, `ring`, `comm_ring`)
• an order class (`partial_order`, `linear_order`)
• assumptions on how both interact ((strict) monotonicity, canonicity)

For short,

• "`+` respects `≤`" means "monotonicity of addition"
• "`*` respects `<`" means "strict monotonicity of multiplication by a positive number".

## Typeclasses #

• `ordered_semiring`: Semiring with a partial order such that `+` respects `≤` and `*` respects `<`.
• `ordered_comm_semiring`: Commutative semiring with a partial order such that `+` respects `≤` and `*` respects `<`.
• `ordered_ring`: Ring with a partial order such that `+` respects `≤` and `*` respects `<`.
• `ordered_comm_ring`: Commutative ring with a partial order such that `+` respects `≤` and `*` respects `<`.
• `linear_ordered_semiring`: Semiring with a linear order such that `+` respects `≤` and `*` respects `<`.
• `linear_ordered_ring`: Ring with a linear order such that `+` respects `≤` and `*` respects `<`.
• `linear_ordered_comm_ring`: Commutative ring with a linear order such that `+` respects `≤` and `*` respects `<`.
• `canonically_ordered_comm_semiring`: Commutative semiring with a partial order such that `+` respects `≤`, `*` respects `<`, and `a ≤ b ↔ ∃ c, b = a + c`.

and some typeclasses to define ordered rings by specifying their nonegative elements:

• `nonneg_ring`: To define `ordered_ring`s.
• `linear_nonneg_ring`: To define `linear_ordered_ring`s.

## 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.

• `ordered_semiring`
• `ordered_cancel_add_comm_monoid` & multiplication & `*` respects `<`
• `semiring` & partial order structure & `+` respects `≤` & `*` respects `<`
• `ordered_comm_semiring`
• `ordered_semiring` & commutativity of multiplication
• `comm_semiring` & partial order structure & `+` respects `≤` & `*` respects `<`
• `ordered_ring`
• `ordered_semiring` & additive inverses
• `ordered_add_comm_group` & multiplication & `*` respects `<`
• `ring` & partial order structure & `+` respects `≤` & `*` respects `<`
• `ordered_comm_ring`
• `ordered_ring` & commutativity of multiplication
• `ordered_comm_semiring` & additive inverses
• `comm_ring` & partial order structure & `+` respects `≤` & `*` respects `<`
• `linear_ordered_semiring`
• `ordered_semiring` & totality of the order & nontriviality
• `linear_ordered_add_comm_monoid` & multiplication & nontriviality & `*` respects `<`
• `linear_ordered_ring`
• `ordered_ring` & totality of the order & nontriviality
• `linear_ordered_semiring` & additive inverses
• `linear_ordered_add_comm_group` & multiplication & `*` respects `<`
• `domain` & linear order structure
• `linear_ordered_comm_ring`
• `ordered_comm_ring` & totality of the order & nontriviality
• `linear_ordered_ring` & commutativity of multiplication
• `integral_domain` & linear order structure
• `canonically_ordered_comm_semiring`
• `canonically_ordered_add_monoid` & multiplication & `*` respects `<` & no zero divisors
• `comm_semiring` & `a ≤ b ↔ ∃ c, b = a + c` & no zero divisors

## TODO #

We're still missing some typeclasses, like

• `linear_ordered_comm_semiring`
• `canonically_ordered_semiring` They have yet to come up in practice.
theorem add_one_le_two_mul {α : Type u} [preorder α] [semiring α] {a : α} (a1 : 1 a) :
a + 1 2 * a
@[instance]
def ordered_semiring.to_semiring (α : Type u) [self : ordered_semiring α] :
@[class]
structure ordered_semiring (α : Type u) :
Type u
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), = 0) . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), = x + . "try_refl_tac"
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), (a * b) * c = a * b * c
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : α → α
• npow_zero' : (∀ (x : α), = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : α), = x * . "try_refl_tac"
• add_left_cancel : ∀ (a b c : α), a + b = a + cb = c
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
• le_antisymm : ∀ (a b : α), a bb aa = b
• add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b
• le_of_add_le_add_left : ∀ (a b c : α), a + b a + cb c
• zero_le_one : 0 1
• mul_lt_mul_of_pos_left : ∀ (a b c : α), a < b0 < cc * a < c * b
• mul_lt_mul_of_pos_right : ∀ (a b c : α), a < b0 < ca * c < b * c

An `ordered_semiring α` is a semiring `α` with a partial order such that addition is monotone and multiplication by a positive number is strictly monotone.

Instances
@[instance]
@[simp]
theorem zero_le_one {α : Type u}  :
0 1
theorem zero_le_two {α : Type u}  :
0 2
theorem one_le_two {α : Type u}  :
1 2
@[simp]
theorem zero_lt_one {α : Type u} [nontrivial α] :
0 < 1
theorem zero_lt_two {α : Type u} [nontrivial α] :
0 < 2
theorem two_ne_zero {α : Type u} [nontrivial α] :
2 0
theorem one_lt_two {α : Type u} [nontrivial α] :
1 < 2
theorem zero_lt_three {α : Type u} [nontrivial α] :
0 < 3
theorem zero_lt_four {α : Type u} [nontrivial α] :
0 < 4
theorem mul_lt_mul_of_pos_left {α : Type u} {a b c : α} (h₁ : a < b) (h₂ : 0 < c) :
c * a < c * b
theorem mul_lt_mul_of_pos_right {α : Type u} {a b c : α} (h₁ : a < b) (h₂ : 0 < c) :
a * c < b * c
theorem decidable.mul_le_mul_of_nonneg_left {α : Type u} {a b c : α} (h₁ : a b) (h₂ : 0 c) :
c * a c * b
theorem mul_le_mul_of_nonneg_left {α : Type u} {a b c : α} :
a b0 cc * a c * b
theorem decidable.mul_le_mul_of_nonneg_right {α : Type u} {a b c : α} (h₁ : a b) (h₂ : 0 c) :
a * c b * c
theorem mul_le_mul_of_nonneg_right {α : Type u} {a b c : α} :
a b0 ca * c b * c
theorem decidable.mul_le_mul {α : Type u} {a b c d : α} (hac : a c) (hbd : b d) (nn_b : 0 b) (nn_c : 0 c) :
a * b c * d
theorem mul_le_mul {α : Type u} {a b c d : α} :
a cb d0 b0 ca * b c * d
theorem decidable.mul_nonneg_le_one_le {α : Type u_1} {a b c : α} (h₁ : 0 c) (h₂ : a c) (h₃ : 0 b) (h₄ : b 1) :
a * b c
theorem mul_nonneg_le_one_le {α : Type u_1} {a b c : α} :
0 ca c0 bb 1a * b c
theorem decidable.mul_nonneg {α : Type u} {a b : α} (ha : 0 a) (hb : 0 b) :
0 a * b
theorem mul_nonneg {α : Type u} {a b : α} :
0 a0 b0 a * b
theorem decidable.mul_nonpos_of_nonneg_of_nonpos {α : Type u} {a b : α} (ha : 0 a) (hb : b 0) :
a * b 0
theorem mul_nonpos_of_nonneg_of_nonpos {α : Type u} {a b : α} :
0 ab 0a * b 0
theorem decidable.mul_nonpos_of_nonpos_of_nonneg {α : Type u} {a b : α} (ha : a 0) (hb : 0 b) :
a * b 0
theorem mul_nonpos_of_nonpos_of_nonneg {α : Type u} {a b : α} :
a 00 ba * b 0
theorem decidable.mul_lt_mul {α : Type u} {a b c d : α} (hac : a < c) (hbd : b d) (pos_b : 0 < b) (nn_c : 0 c) :
a * b < c * d
theorem mul_lt_mul {α : Type u} {a b c d : α} :
a < cb d0 < b0 ca * b < c * d
theorem decidable.mul_lt_mul' {α : Type u} {a b c d : α} (h1 : a c) (h2 : b < d) (h3 : 0 b) (h4 : 0 < c) :
a * b < c * d
theorem mul_lt_mul' {α : Type u} {a b c d : α} :
a cb < d0 b0 < ca * b < c * d
theorem mul_pos {α : Type u} {a b : α} (ha : 0 < a) (hb : 0 < b) :
0 < a * b
theorem mul_neg_of_pos_of_neg {α : Type u} {a b : α} (ha : 0 < a) (hb : b < 0) :
a * b < 0
theorem mul_neg_of_neg_of_pos {α : Type u} {a b : α} (ha : a < 0) (hb : 0 < b) :
a * b < 0
theorem decidable.mul_self_lt_mul_self {α : Type u} {a b : α} (h1 : 0 a) (h2 : a < b) :
a * a < b * b
theorem mul_self_lt_mul_self {α : Type u} {a b : α} (h1 : 0 a) (h2 : a < b) :
a * a < b * b
theorem decidable.strict_mono_incr_on_mul_self {α : Type u}  :
strict_mono_incr_on (λ (x : α), x * x) (set.Ici 0)
theorem strict_mono_incr_on_mul_self {α : Type u}  :
strict_mono_incr_on (λ (x : α), x * x) (set.Ici 0)
theorem decidable.mul_self_le_mul_self {α : Type u} {a b : α} (h1 : 0 a) (h2 : a b) :
a * a b * b
theorem mul_self_le_mul_self {α : Type u} {a b : α} (h1 : 0 a) (h2 : a b) :
a * a b * b
theorem decidable.mul_lt_mul'' {α : Type u} {a b c d : α} (h1 : a < c) (h2 : b < d) (h3 : 0 a) (h4 : 0 b) :
a * b < c * d
theorem mul_lt_mul'' {α : Type u} {a b c d : α} :
a < cb < d0 a0 ba * b < c * d
theorem decidable.le_mul_of_one_le_right {α : Type u} {a b : α} (hb : 0 b) (h : 1 a) :
b b * a
theorem le_mul_of_one_le_right {α : Type u} {a b : α} :
0 b1 ab b * a
theorem decidable.le_mul_of_one_le_left {α : Type u} {a b : α} (hb : 0 b) (h : 1 a) :
b a * b
theorem le_mul_of_one_le_left {α : Type u} {a b : α} :
0 b1 ab a * b
theorem decidable.lt_mul_of_one_lt_right {α : Type u} {a b : α} (hb : 0 < b) (h : 1 < a) :
b < b * a
theorem lt_mul_of_one_lt_right {α : Type u} {a b : α} :
0 < b1 < ab < b * a
theorem decidable.lt_mul_of_one_lt_left {α : Type u} {a b : α} (hb : 0 < b) (h : 1 < a) :
b < a * b
theorem lt_mul_of_one_lt_left {α : Type u} {a b : α} :
0 < b1 < ab < a * b
theorem decidable.add_le_mul_two_add {α : Type u} {a b : α} (a2 : 2 a) (b0 : 0 b) :
a + (2 + b) a * (2 + b)
theorem add_le_mul_two_add {α : Type u} {a b : α} :
2 a0 ba + (2 + b) a * (2 + b)
theorem decidable.one_le_mul_of_one_le_of_one_le {α : Type u} {a b : α} (a1 : 1 a) (b1 : 1 b) :
1 a * b
theorem one_le_mul_of_one_le_of_one_le {α : Type u} {a b : α} :
1 a1 b1 a * b
def function.injective.ordered_semiring {α : Type u} {β : Type u_1} [has_zero β] [has_one β] [has_add β] [has_mul β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) :

Pullback an `ordered_semiring` under an injective map. See note [reducible non-instances].

Equations
theorem bit1_pos {α : Type u} {a : α} [nontrivial α] (h : 0 a) :
0 < bit1 a
theorem lt_add_one {α : Type u} [nontrivial α] (a : α) :
a < a + 1
theorem lt_one_add {α : Type u} [nontrivial α] (a : α) :
a < 1 + a
theorem bit1_pos' {α : Type u} {a : α} (h : 0 < a) :
0 < bit1 a
theorem decidable.one_lt_mul {α : Type u} {a b : α} (ha : 1 a) (hb : 1 < b) :
1 < a * b
theorem one_lt_mul {α : Type u} {a b : α} :
1 a1 < b1 < a * b
theorem decidable.mul_le_one {α : Type u} {a b : α} (ha : a 1) (hb' : 0 b) (hb : b 1) :
a * b 1
theorem mul_le_one {α : Type u} {a b : α} :
a 10 bb 1a * b 1
theorem decidable.one_lt_mul_of_le_of_lt {α : Type u} {a b : α} (ha : 1 a) (hb : 1 < b) :
1 < a * b
theorem one_lt_mul_of_le_of_lt {α : Type u} {a b : α} :
1 a1 < b1 < a * b
theorem decidable.one_lt_mul_of_lt_of_le {α : Type u} {a b : α} (ha : 1 < a) (hb : 1 b) :
1 < a * b
theorem one_lt_mul_of_lt_of_le {α : Type u} {a b : α} :
1 < a1 b1 < a * b
theorem decidable.mul_le_of_le_one_right {α : Type u} {a b : α} (ha : 0 a) (hb1 : b 1) :
a * b a
theorem mul_le_of_le_one_right {α : Type u} {a b : α} :
0 ab 1a * b a
theorem decidable.mul_le_of_le_one_left {α : Type u} {a b : α} (hb : 0 b) (ha1 : a 1) :
a * b b
theorem mul_le_of_le_one_left {α : Type u} {a b : α} :
0 ba 1a * b b
theorem decidable.mul_lt_one_of_nonneg_of_lt_one_left {α : Type u} {a b : α} (ha0 : 0 a) (ha : a < 1) (hb : b 1) :
a * b < 1
theorem mul_lt_one_of_nonneg_of_lt_one_left {α : Type u} {a b : α} :
0 aa < 1b 1a * b < 1
theorem decidable.mul_lt_one_of_nonneg_of_lt_one_right {α : Type u} {a b : α} (ha : a 1) (hb0 : 0 b) (hb : b < 1) :
a * b < 1
theorem mul_lt_one_of_nonneg_of_lt_one_right {α : Type u} {a b : α} :
a 10 bb < 1a * b < 1
@[instance]
@[instance]
@[class]
structure ordered_comm_semiring (α : Type u) :
Type u
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), (a * b) * c = a * b * c
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : α → α
• npow_zero' : (∀ (x : α), . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• add_left_cancel : ∀ (a b c : α), a + b = a + cb = c
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
• le_antisymm : ∀ (a b : α), a bb aa = b
• add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b
• le_of_add_le_add_left : ∀ (a b c : α), a + b a + cb c
• zero_le_one : 0 1
• mul_lt_mul_of_pos_left : ∀ (a b c : α), a < b0 < cc * a < c * b
• mul_lt_mul_of_pos_right : ∀ (a b c : α), a < b0 < ca * c < b * c
• mul_comm : ∀ (a b : α), a * b = b * a

An `ordered_comm_semiring α` is a commutative semiring `α` with a partial order such that addition is monotone and multiplication by a positive number is strictly monotone.

Instances
def function.injective.ordered_comm_semiring {α : Type u} {β : Type u_1} [has_zero β] [has_one β] [has_add β] [has_mul β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) :

Pullback an `ordered_comm_semiring` under an injective map. See note [reducible non-instances].

Equations
@[instance]
@[class]
structure linear_ordered_semiring (α : Type u) :
Type u
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), (a * b) * c = a * b * c
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : α → α
• npow_zero' : (∀ (x : α), . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• add_left_cancel : ∀ (a b c : α), a + b = a + cb = c
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
• le_antisymm : ∀ (a b : α), a bb aa = b
• add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b
• le_of_add_le_add_left : ∀ (a b c : α), a + b a + cb c
• zero_le_one : 0 1
• mul_lt_mul_of_pos_left : ∀ (a b c : α), a < b0 < cc * a < c * b
• mul_lt_mul_of_pos_right : ∀ (a b c : α), a < b0 < ca * c < b * c
• le_total : ∀ (a b : α), a b b a
• decidable_le :
• decidable_eq :
• decidable_lt :
• max : α → α → α
• max_def : . "reflexivity"
• min : α → α → α
• min_def : . "reflexivity"
• exists_pair_ne : ∃ (x y : α), x y

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
@[instance]
theorem zero_lt_one' {α : Type u}  :
0 < 1
theorem lt_of_mul_lt_mul_left {α : Type u} {a b c : α} (h : c * a < c * b) (hc : 0 c) :
a < b
theorem lt_of_mul_lt_mul_right {α : Type u} {a b c : α} (h : a * c < b * c) (hc : 0 c) :
a < b
theorem le_of_mul_le_mul_left {α : Type u} {a b c : α} (h : c * a c * b) (hc : 0 < c) :
a b
theorem le_of_mul_le_mul_right {α : Type u} {a b c : α} (h : a * c b * c) (hc : 0 < c) :
a b
theorem pos_and_pos_or_neg_and_neg_of_mul_pos {α : Type u} {a b : α} (hab : 0 < a * b) :
0 < a 0 < b a < 0 b < 0
theorem nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nnonneg {α : Type u} {a b : α} (hab : 0 a * b) :
0 a 0 b a 0 b 0
theorem pos_of_mul_pos_left {α : Type u} {a b : α} (h : 0 < a * b) (ha : 0 a) :
0 < b
theorem pos_of_mul_pos_right {α : Type u} {a b : α} (h : 0 < a * b) (hb : 0 b) :
0 < a
@[simp]
theorem inv_of_pos {α : Type u} {a : α} [invertible a] :
0 < a 0 < a
@[simp]
theorem inv_of_nonpos {α : Type u} {a : α} [invertible a] :
a 0 a 0
theorem nonneg_of_mul_nonneg_left {α : Type u} {a b : α} (h : 0 a * b) (h1 : 0 < a) :
0 b
theorem nonneg_of_mul_nonneg_right {α : Type u} {a b : α} (h : 0 a * b) (h1 : 0 < b) :
0 a
@[simp]
theorem inv_of_nonneg {α : Type u} {a : α} [invertible a] :
0 a 0 a
@[simp]
theorem inv_of_lt_zero {α : Type u} {a : α} [invertible a] :
a < 0 a < 0
@[simp]
theorem inv_of_le_one {α : Type u} {a : α} [invertible a] (h : 1 a) :
a 1
theorem neg_of_mul_neg_left {α : Type u} {a b : α} (h : a * b < 0) (h1 : 0 a) :
b < 0
theorem neg_of_mul_neg_right {α : Type u} {a b : α} (h : a * b < 0) (h1 : 0 b) :
a < 0
theorem nonpos_of_mul_nonpos_left {α : Type u} {a b : α} (h : a * b 0) (h1 : 0 < a) :
b 0
theorem nonpos_of_mul_nonpos_right {α : Type u} {a b : α} (h : a * b 0) (h1 : 0 < b) :
a 0
@[simp]
theorem mul_le_mul_left {α : Type u} {a b c : α} (h : 0 < c) :
c * a c * b a b
@[simp]
theorem mul_le_mul_right {α : Type u} {a b c : α} (h : 0 < c) :
a * c b * c a b
@[simp]
theorem mul_lt_mul_left {α : Type u} {a b c : α} (h : 0 < c) :
c * a < c * b a < b
@[simp]
theorem mul_lt_mul_right {α : Type u} {a b c : α} (h : 0 < c) :
a * c < b * c a < b
@[simp]
theorem zero_le_mul_left {α : Type u} {b c : α} (h : 0 < c) :
0 c * b 0 b
@[simp]
theorem zero_le_mul_right {α : Type u} {b c : α} (h : 0 < c) :
0 b * c 0 b
@[simp]
theorem zero_lt_mul_left {α : Type u} {b c : α} (h : 0 < c) :
0 < c * b 0 < b
@[simp]
theorem zero_lt_mul_right {α : Type u} {b c : α} (h : 0 < c) :
0 < b * c 0 < b
theorem add_le_mul_of_left_le_right {α : Type u} {a b : α} (a2 : 2 a) (ab : a b) :
a + b a * b
theorem add_le_mul_of_right_le_left {α : Type u} {a b : α} (b2 : 2 b) (ba : b a) :
a + b a * b
theorem add_le_mul {α : Type u} {a b : α} (a2 : 2 a) (b2 : 2 b) :
a + b a * b
theorem add_le_mul' {α : Type u} {a b : α} (a2 : 2 a) (b2 : 2 b) :
a + b b * a
@[simp]
theorem bit0_le_bit0 {α : Type u} {a b : α} [nontrivial α] :
bit0 a bit0 b a b
@[simp]
theorem bit0_lt_bit0 {α : Type u} {a b : α} [nontrivial α] :
bit0 a < bit0 b a < b
@[simp]
theorem bit1_le_bit1 {α : Type u} {a b : α} [nontrivial α] :
bit1 a bit1 b a b
@[simp]
theorem bit1_lt_bit1 {α : Type u} {a b : α} [nontrivial α] :
bit1 a < bit1 b a < b
@[simp]
theorem one_le_bit1 {α : Type u} {a : α} [nontrivial α] :
1 bit1 a 0 a
@[simp]
theorem one_lt_bit1 {α : Type u} {a : α} [nontrivial α] :
1 < bit1 a 0 < a
@[simp]
theorem zero_le_bit0 {α : Type u} {a : α} [nontrivial α] :
0 bit0 a 0 a
@[simp]
theorem zero_lt_bit0 {α : Type u} {a : α} [nontrivial α] :
0 < bit0 a 0 < a
theorem le_mul_iff_one_le_left {α : Type u} {a b : α} (hb : 0 < b) :
b a * b 1 a
theorem lt_mul_iff_one_lt_left {α : Type u} {a b : α} (hb : 0 < b) :
b < a * b 1 < a
theorem le_mul_iff_one_le_right {α : Type u} {a b : α} (hb : 0 < b) :
b b * a 1 a
theorem lt_mul_iff_one_lt_right {α : Type u} {a b : α} (hb : 0 < b) :
b < b * a 1 < a
theorem mul_nonneg_iff_right_nonneg_of_pos {α : Type u} {a b : α} (ha : 0 < a) :
0 b * a 0 b
theorem mul_le_iff_le_one_left {α : Type u} {a b : α} (hb : 0 < b) :
a * b b a 1
theorem mul_lt_iff_lt_one_left {α : Type u} {a b : α} (hb : 0 < b) :
a * b < b a < 1
theorem mul_le_iff_le_one_right {α : Type u} {a b : α} (hb : 0 < b) :
b * a b a 1
theorem mul_lt_iff_lt_one_right {α : Type u} {a b : α} (hb : 0 < b) :
b * a < b a < 1
theorem nonpos_of_mul_nonneg_left {α : Type u} {a b : α} (h : 0 a * b) (hb : b < 0) :
a 0
theorem nonpos_of_mul_nonneg_right {α : Type u} {a b : α} (h : 0 a * b) (ha : a < 0) :
b 0
theorem neg_of_mul_pos_left {α : Type u} {a b : α} (h : 0 < a * b) (hb : b 0) :
a < 0
theorem neg_of_mul_pos_right {α : Type u} {a b : α} (h : 0 < a * b) (ha : a 0) :
b < 0
@[instance]
def linear_ordered_semiring.to_no_top_order {α : Type u_1}  :
def function.injective.linear_ordered_semiring {α : Type u} {β : Type u_1} [has_zero β] [has_one β] [has_add β] [has_mul β] [nontrivial β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) :

Pullback a `linear_ordered_semiring` under an injective map. See note [reducible non-instances].

Equations
theorem monotone_mul_left_of_nonneg {α : Type u} {a : α} (ha : 0 a) :
monotone (λ (x : α), a * x)
theorem monotone_mul_right_of_nonneg {α : Type u} {a : α} (ha : 0 a) :
monotone (λ (x : α), x * a)
theorem monotone.mul_const {α : Type u} {β : Type u_1} [preorder β] {f : β → α} {a : α} (hf : monotone f) (ha : 0 a) :
monotone (λ (x : β), (f x) * a)
theorem monotone.const_mul {α : Type u} {β : Type u_1} [preorder β] {f : β → α} {a : α} (hf : monotone f) (ha : 0 a) :
monotone (λ (x : β), a * f x)
theorem monotone.mul {α : Type u} {β : Type u_1} [preorder β] {f g : β → α} (hf : monotone f) (hg : monotone g) (hf0 : ∀ (x : β), 0 f x) (hg0 : ∀ (x : β), 0 g x) :
monotone (λ (x : β), (f x) * g x)
theorem strict_mono_mul_left_of_pos {α : Type u} {a : α} (ha : 0 < a) :
strict_mono (λ (x : α), a * x)
theorem strict_mono_mul_right_of_pos {α : Type u} {a : α} (ha : 0 < a) :
strict_mono (λ (x : α), x * a)
theorem strict_mono.mul_const {α : Type u} {β : Type u_1} [preorder β] {f : β → α} {a : α} (hf : strict_mono f) (ha : 0 < a) :
strict_mono (λ (x : β), (f x) * a)
theorem strict_mono.const_mul {α : Type u} {β : Type u_1} [preorder β] {f : β → α} {a : α} (hf : strict_mono f) (ha : 0 < a) :
strict_mono (λ (x : β), a * f x)
theorem strict_mono.mul_monotone {α : Type u} {β : Type u_1} [preorder β] {f g : β → α} (hf : strict_mono f) (hg : monotone g) (hf0 : ∀ (x : β), 0 f x) (hg0 : ∀ (x : β), 0 < g x) :
strict_mono (λ (x : β), (f x) * g x)
theorem monotone.mul_strict_mono {α : Type u} {β : Type u_1} [preorder β] {f g : β → α} (hf : monotone f) (hg : strict_mono g) (hf0 : ∀ (x : β), 0 < f x) (hg0 : ∀ (x : β), 0 g x) :
strict_mono (λ (x : β), (f x) * g x)
theorem strict_mono.mul {α : Type u} {β : Type u_1} [preorder β] {f g : β → α} (hf : strict_mono f) (hg : strict_mono g) (hf0 : ∀ (x : β), 0 f x) (hg0 : ∀ (x : β), 0 g x) :
strict_mono (λ (x : β), (f x) * g x)
theorem mul_max_of_nonneg {α : Type u} {a : α} (b c : α) (ha : 0 a) :
a * max b c = max (a * b) (a * c)
theorem mul_min_of_nonneg {α : Type u} {a : α} (b c : α) (ha : 0 a) :
a * min b c = min (a * b) (a * c)
theorem max_mul_of_nonneg {α : Type u} {c : α} (a b : α) (hc : 0 c) :
(max a b) * c = max (a * c) (b * c)
theorem min_mul_of_nonneg {α : Type u} {c : α} (a b : α) (hc : 0 c) :
(min a b) * c = min (a * c) (b * c)
@[instance]
def ordered_ring.to_ordered_add_comm_group (α : Type u) [self : ordered_ring α] :
@[class]
structure ordered_ring (α : Type u) :
Type u
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), = 0) . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), = x + . "try_refl_tac"
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
• gsmul : α → α
• gsmul_zero' : (∀ (a : α), = 0) . "try_refl_tac"
• gsmul_succ' : (∀ (n : ) (a : α), = a + a) . "try_refl_tac"
• gsmul_neg' : (∀ (n : ) (a : α), = - a) . "try_refl_tac"
• add_left_neg : ∀ (a : α), -a + a = 0
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• mul_assoc : ∀ (a b c : α), (a * b) * c = a * b * c
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : α → α
• npow_zero' : (∀ (x : α), = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : α), = x * . "try_refl_tac"
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
• le_antisymm : ∀ (a b : α), a bb aa = b
• add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b
• zero_le_one : 0 1
• mul_pos : ∀ (a b : α), 0 < a0 < b0 < a * b

An `ordered_ring α` is a ring `α` with a partial order such that addition is monotone and multiplication by a positive number is strictly monotone.

Instances
@[instance]
def ordered_ring.to_ring (α : Type u) [self : ordered_ring α] :
ring α
theorem decidable.ordered_ring.mul_nonneg {α : Type u} [ordered_ring α] {a b : α} (h₁ : 0 a) (h₂ : 0 b) :
0 a * b
theorem ordered_ring.mul_nonneg {α : Type u} [ordered_ring α] {a b : α} :
0 a0 b0 a * b
theorem decidable.ordered_ring.mul_le_mul_of_nonneg_left {α : Type u} [ordered_ring α] {a b c : α} (h₁ : a b) (h₂ : 0 c) :
c * a c * b
theorem ordered_ring.mul_le_mul_of_nonneg_left {α : Type u} [ordered_ring α] {a b c : α} :
a b0 cc * a c * b
theorem decidable.ordered_ring.mul_le_mul_of_nonneg_right {α : Type u} [ordered_ring α] {a b c : α} (h₁ : a b) (h₂ : 0 c) :
a * c b * c
theorem ordered_ring.mul_le_mul_of_nonneg_right {α : Type u} [ordered_ring α] {a b c : α} :
a b0 ca * c b * c
theorem ordered_ring.mul_lt_mul_of_pos_left {α : Type u} [ordered_ring α] {a b c : α} (h₁ : a < b) (h₂ : 0 < c) :
c * a < c * b
theorem ordered_ring.mul_lt_mul_of_pos_right {α : Type u} [ordered_ring α] {a b c : α} (h₁ : a < b) (h₂ : 0 < c) :
a * c < b * c
theorem decidable.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_left {α : Type u} [ordered_ring α] {a b c : α} :
b ac 0c * a c * b
theorem decidable.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_le_mul_of_nonpos_right {α : Type u} [ordered_ring α] {a b c : α} :
b ac 0a * c b * c
theorem decidable.mul_nonneg_of_nonpos_of_nonpos {α : Type u} [ordered_ring α] {a b : α} (ha : a 0) (hb : b 0) :
0 a * b
theorem mul_nonneg_of_nonpos_of_nonpos {α : Type u} [ordered_ring α] {a b : α} :
a 0b 00 a * b
theorem mul_lt_mul_of_neg_left {α : Type u} [ordered_ring α] {a b c : α} (h : b < a) (hc : c < 0) :
c * a < c * b
theorem mul_lt_mul_of_neg_right {α : Type u} [ordered_ring α] {a b c : α} (h : b < a) (hc : c < 0) :
a * c < b * c
theorem mul_pos_of_neg_of_neg {α : Type u} [ordered_ring α] {a b : α} (ha : a < 0) (hb : b < 0) :
0 < a * b
def function.injective.ordered_ring {α : Type u} [ordered_ring α] {β : Type u_1} [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) (neg : ∀ (x : β), f (-x) = -f x) (sub : ∀ (x y : β), f (x - y) = f x - f y) :

Pullback an `ordered_ring` under an injective map. See note [reducible non-instances].

Equations
@[instance]
def ordered_comm_ring.to_comm_ring (α : Type u) [self : ordered_comm_ring α] :
@[instance]
def ordered_comm_ring.to_ordered_ring (α : Type u) [self : ordered_comm_ring α] :
@[class]
structure ordered_comm_ring (α : Type u) :
Type u
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), = 0) . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), = x + . "try_refl_tac"
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
• gsmul : α → α
• gsmul_zero' : (∀ (a : α), = 0) . "try_refl_tac"
• gsmul_succ' : (∀ (n : ) (a : α), = a + . "try_refl_tac"
• gsmul_neg' : (∀ (n : ) (a : α), . "try_refl_tac"
• add_left_neg : ∀ (a : α), -a + a = 0
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• mul_assoc : ∀ (a b c : α), (a * b) * c = a * b * c
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : α → α
• npow_zero' : (∀ (x : α), = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : α), = x * . "try_refl_tac"
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
• le_antisymm : ∀ (a b : α), a bb aa = b
• add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b
• zero_le_one : 0 1
• mul_pos : ∀ (a b : α), 0 < a0 < b0 < a * b
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• add_left_cancel : ∀ (a b c : α), a + b = a + cb = c
• le_of_add_le_add_left : ∀ (a b c : α), a + b a + cb c
• mul_lt_mul_of_pos_left : ∀ (a b c : α), a < b0 < cc * a < c * b
• mul_lt_mul_of_pos_right : ∀ (a b c : α), a < b0 < ca * c < b * c
• mul_comm : ∀ (a b : α), a * b = b * a

An `ordered_comm_ring α` is a commutative ring `α` with a partial order such that addition is monotone and multiplication by a positive number is strictly monotone.

Instances
@[instance]
def function.injective.ordered_comm_ring {α : Type u} {β : Type u_1} [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) (neg : ∀ (x : β), f (-x) = -f x) (sub : ∀ (x y : β), f (x - y) = f x - f y) :

Pullback an `ordered_comm_ring` under an injective map. See note [reducible non-instances].

Equations
@[instance]
def linear_ordered_ring.to_nontrivial (α : Type u) [self : linear_ordered_ring α] :
@[instance]
def linear_ordered_ring.to_linear_order (α : Type u) [self : linear_ordered_ring α] :
@[class]
structure linear_ordered_ring (α : Type u) :
Type u
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
• gsmul : α → α
• gsmul_zero' : (∀ (a : α), . "try_refl_tac"
• gsmul_succ' : (∀ (n : ) (a : α), = a + . "try_refl_tac"
• gsmul_neg' : (∀ (n : ) (a : α), . "try_refl_tac"
• add_left_neg : ∀ (a : α), -a + a = 0
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• mul_assoc : ∀ (a b c : α), (a * b) * c = a * b * c
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : α → α
• npow_zero' : (∀ (x : α), . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
• le_antisymm : ∀ (a b : α), a bb aa = b
• add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b
• zero_le_one : 0 1
• mul_pos : ∀ (a b : α), 0 < a0 < b0 < a * b
• le_total : ∀ (a b : α), a b b a
• decidable_le :
• decidable_eq :
• decidable_lt :
• max : α → α → α
• max_def : . "reflexivity"
• min : α → α → α
• min_def : . "reflexivity"
• exists_pair_ne : ∃ (x y : α), x y

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
@[instance]
def linear_ordered_ring.to_ordered_ring (α : Type u) [self : linear_ordered_ring α] :
@[instance]
Equations
@[simp]
theorem abs_one {α : Type u}  :
abs 1 = 1
@[simp]
theorem abs_two {α : Type u}  :
abs 2 = 2
theorem abs_mul {α : Type u} (a b : α) :
abs (a * b) = (abs a) * abs b
def abs_hom {α : Type u}  :

`abs` as a `monoid_with_zero_hom`.

Equations
@[simp]
theorem abs_mul_abs_self {α : Type u} (a : α) :
(abs a) * abs a = a * a
@[simp]
theorem abs_mul_self {α : Type u} (a : α) :
abs (a * a) = a * a
theorem mul_pos_iff {α : Type u} {a b : α} :
0 < a * b 0 < a 0 < b a < 0 b < 0
theorem mul_neg_iff {α : Type u} {a b : α} :
a * b < 0 0 < a b < 0 a < 0 0 < b
theorem mul_nonneg_iff {α : Type u} {a b : α} :
0 a * b 0 a 0 b a 0 b 0
theorem mul_nonneg_of_three {α : Type u} (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} {a b : α} :
a * b 0 0 a b 0 a 0 0 b
theorem mul_self_nonneg {α : Type u} (a : α) :
0 a * a
@[simp]
theorem neg_le_self_iff {α : Type u} {a : α} :
-a a 0 a
@[simp]
theorem neg_lt_self_iff {α : Type u} {a : α} :
-a < a 0 < a
@[simp]
theorem le_neg_self_iff {α : Type u} {a : α} :
a -a a 0
@[simp]
theorem lt_neg_self_iff {α : Type u} {a : α} :
a < -a a < 0
@[simp]
theorem abs_eq_self {α : Type u} {a : α} :
abs a = a 0 a
@[simp]
theorem abs_eq_neg_self {α : Type u} {a : α} :
abs a = -a a 0
theorem abs_cases {α : Type u} (a : α) :
abs a = a 0 a abs a = -a a < 0

For an element `a` of a linear ordered ring, either `abs a = a` and `0 ≤ a`, or `abs a = -a` and `a < 0`. Use cases on this lemma to automate linarith in inequalities

theorem gt_of_mul_lt_mul_neg_left {α : Type u} {a b c : α} (h : c * a < c * b) (hc : c 0) :
b < a
theorem neg_one_lt_zero {α : Type u}  :
-1 < 0
theorem le_of_mul_le_of_one_le {α : Type u} {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} {a b : α} (hb : 0 b) (h : a * a b * b) :
a b
theorem mul_self_le_mul_self_iff {α : Type u} {a b : α} (h1 : 0 a) (h2 : 0 b) :
a b a * a b * b
theorem mul_self_lt_mul_self_iff {α : Type u} {a b : α} (h1 : 0 a) (h2 : 0 b) :
a < b a * a < b * b
theorem mul_self_inj {α : Type u} {a b : α} (h1 : 0 a) (h2 : 0 b) :
a * a = b * b a = b
@[simp]
theorem mul_le_mul_left_of_neg {α : Type u} {a b c : α} (h : c < 0) :
c * a c * b b a
@[simp]
theorem mul_le_mul_right_of_neg {α : Type u} {a b c : α} (h : c < 0) :
a * c b * c b a
@[simp]
theorem mul_lt_mul_left_of_neg {α : Type u} {a b c : α} (h : c < 0) :
c * a < c * b b < a
@[simp]
theorem mul_lt_mul_right_of_neg {α : Type u} {a b c : α} (h : c < 0) :
a * c < b * c b < a
theorem sub_one_lt {α : Type u} (a : α) :
a - 1 < a
theorem mul_self_pos {α : Type u} {a : α} (ha : a 0) :
0 < a * a
theorem mul_self_le_mul_self_of_le_of_neg_le {α : Type u} {x y : α} (h₁ : x y) (h₂ : -x y) :
x * x y * y
theorem nonneg_of_mul_nonpos_left {α : Type u} {a b : α} (h : a * b 0) (hb : b < 0) :
0 a
theorem nonneg_of_mul_nonpos_right {α : Type u} {a b : α} (h : a * b 0) (ha : a < 0) :
0 b
theorem pos_of_mul_neg_left {α : Type u} {a b : α} (h : a * b < 0) (hb : b 0) :
0 < a
theorem pos_of_mul_neg_right {α : Type u} {a b : α} (h : a * b < 0) (ha : a 0) :
0 < b
theorem mul_self_add_mul_self_eq_zero {α : Type u} {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} {a b : α} (h : a * a + b * b = 0) :
a = 0
theorem abs_eq_iff_mul_self_eq {α : Type u} {a b : α} :
abs a = abs b a * a = b * b
theorem abs_lt_iff_mul_self_lt {α : Type u} {a b : α} :
abs a < abs b a * a < b * b
theorem abs_le_iff_mul_self_le {α : Type u} {a b : α} :
abs a abs b a * a b * b
theorem abs_le_one_iff_mul_self_le_one {α : Type u} {a : α} :
abs a 1 a * a 1
def function.injective.linear_ordered_ring {α : Type u} {β : Type u_1} [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [nontrivial β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) (neg : ∀ (x : β), f (-x) = -f x) (sub : ∀ (x y : β), f (x - y) = f x - f y) :

Pullback a `linear_ordered_ring` under an injective map. See note [reducible non-instances].

Equations
@[class]
structure linear_ordered_comm_ring (α : Type u) :
Type u
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
• gsmul : α → α
• gsmul_zero' : (∀ (a : α), . "try_refl_tac"
• gsmul_succ' : (∀ (n : ) (a : α), . "try_refl_tac"
• gsmul_neg' : (∀ (n : ) (a : α), . "try_refl_tac"
• add_left_neg : ∀ (a : α), -a + a = 0
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• mul_assoc : ∀ (a b c : α), (a * b) * c = a * b * c
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : α → α
• npow_zero' : (∀ (x : α), . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
• le_antisymm : ∀ (a b : α), a bb aa = b
• add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b
• zero_le_one : 0 1
• mul_pos : ∀ (a b : α), 0 < a0 < b0 < a * b
• le_total : ∀ (a b : α), a b b a
• decidable_le :
• decidable_eq :
• decidable_lt :
• max : α → α → α
• max_def : . "reflexivity"
• min : α → α → α
• min_def : . "reflexivity"
• exists_pair_ne : ∃ (x y : α), x y
• mul_comm : ∀ (a b : α), a * b = b * a

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
@[instance]
theorem max_mul_mul_le_max_mul_max {α : Type u} {a d : α} (b c : α) (ha : 0 a) (hd : 0 d) :
max (a * b) (d * c) (max a c) * max d b
theorem abs_sub_sq {α : Type u} (a b : α) :
(abs (a - b)) * abs (a - b) = a * a + b * b - ((1 + 1) * a) * b
@[simp]
theorem abs_dvd {α : Type u} (a b : α) :
abs a b a b
theorem abs_dvd_self {α : Type u} (a : α) :
abs a a
@[simp]
theorem dvd_abs {α : Type u} (a b : α) :
a abs b a b
theorem self_dvd_abs {α : Type u} (a : α) :
a abs a
theorem abs_dvd_abs {α : Type u} (a b : α) :
abs a abs b a b
theorem even_abs {α : Type u} {a : α} :
def function.injective.linear_ordered_comm_ring {α : Type u} {β : Type u_1} [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [nontrivial β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) (neg : ∀ (x : β), f (-x) = -f x) (sub : ∀ (x y : β), f (x - y) = f x - f y) :

Pullback a `linear_ordered_comm_ring` under an injective map. See note [reducible non-instances].

Equations
@[instance]
def nonneg_ring.to_ring (α : Type u_1) [self : nonneg_ring α] :
ring α
@[class]
structure nonneg_ring (α : Type u_1) :
Type u_1
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), = 0) . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), = x + . "try_refl_tac"
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
• gsmul : α → α
• gsmul_zero' : (∀ (a : α), = 0) . "try_refl_tac"
• gsmul_succ' : (∀ (n : ) (a : α), = a + a) . "try_refl_tac"
• gsmul_neg' : (∀ (n : ) (a : α), = - a) . "try_refl_tac"
• add_left_neg : ∀ (a : α), -a + a = 0
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• mul_assoc : ∀ (a b c : α), (a * b) * c = a * b * c
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : α → α
• npow_zero' : (∀ (x : α), = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : α), = x * x) . "try_refl_tac"
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• nonneg : α → Prop
• pos : α → Prop
• pos_iff : (∀ (a : α), . "order_laws_tac"
• zero_nonneg :
• add_nonneg : ∀ {a b : α}, nonneg_ring.nonneg (a + b)
• nonneg_antisymm : ∀ {a : α}, a = 0
• one_nonneg :
• mul_nonneg : ∀ {a b : α}, nonneg_ring.nonneg (a * b)
• mul_pos : ∀ {a b : α}, nonneg_ring.pos (a * b)

Extend `nonneg_add_comm_group` to support ordered rings specified by their nonnegative elements

Instances
@[instance]
def nonneg_ring.to_nonneg_add_comm_group (α : Type u_1) [self : nonneg_ring α] :
@[class]
structure linear_nonneg_ring (α : Type u_1) :
Type u_1
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
• gsmul : α → α
• gsmul_zero' : (∀ (a : α), . "try_refl_tac"
• gsmul_succ' : (∀ (n : ) (a : α), = a + . "try_refl_tac"
• gsmul_neg' : (∀ (n : ) (a : α), . "try_refl_tac"
• add_left_neg : ∀ (a : α), -a + a = 0
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• mul_assoc : ∀ (a b c : α), (a * b) * c = a * b * c
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : α → α
• npow_zero' : (∀ (x : α), = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : α), = x * . "try_refl_tac"
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• exists_pair_ne : ∃ (x y : α), x y
• eq_zero_or_eq_zero_of_mul_eq_zero : ∀ (a b : α), a * b = 0a = 0 b = 0
• nonneg : α → Prop
• pos : α → Prop
• pos_iff : (∀ (a : α), . "order_laws_tac"
• zero_nonneg :
• add_nonneg : ∀ {a b : α},
• nonneg_antisymm : ∀ {a : α}, a = 0
• one_pos :
• mul_nonneg : ∀ {a b : α},
• nonneg_total : ∀ (a : α),
• dec_nonneg :

Extend `nonneg_add_comm_group` to support linearly ordered rings specified by their nonnegative elements

@[instance]
def linear_nonneg_ring.to_domain (α : Type u_1) [self : linear_nonneg_ring α] :
@[instance]
def nonneg_ring.to_linear_nonneg_ring {α : Type u} [nonneg_ring α] [nontrivial α] (nonneg_total : ∀ (a : α), ) :

`to_linear_nonneg_ring` shows that a `nonneg_ring` with a linear order is a `domain`, hence a `linear_nonneg_ring`.

Equations

Construct `linear_order` from `linear_nonneg_ring`. This is not an instance because we don't use it in `mathlib`.

Equations

Construct `linear_ordered_ring` from `linear_nonneg_ring`. This is not an instance because we don't use it in `mathlib`.

Equations

Convert a `linear_nonneg_ring` with a commutative multiplication and decidable non-negativity into a `linear_ordered_comm_ring`

Equations
@[class]
structure canonically_ordered_comm_semiring (α : Type u_1) :
Type u_1
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• add_comm : ∀ (a b : α), a + b = b + a
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
• le_antisymm : ∀ (a b : α), a bb aa = b
• add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b
• bot : α
• bot_le : ∀ (a : α), a
• le_iff_exists_add : ∀ (a b : α), a b ∃ (c : α), b = a + c
• mul : α → α → α
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), (a * b) * c = a * b * c
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : α → α
• npow_zero' : (∀ (x : α), . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• mul_comm : ∀ (a b : α), a * b = b * a
• eq_zero_or_eq_zero_of_mul_eq_zero : ∀ (a b : α), a * b = 0a = 0 b = 0

A canonically ordered commutative semiring is an ordered, commutative semiring in which `a ≤ b` iff there exists `c` with `b = a + c`. This is satisfied by the natural numbers, for example, but not the integers or other ordered groups.

Instances
@[instance]
@[instance]
@[instance]
theorem canonically_ordered_comm_semiring.zero_lt_one {α : Type u} [nontrivial α] :
0 < 1

A version of `zero_lt_one : 0 < 1` for a `canonically_ordered_comm_semiring`.

theorem canonically_ordered_comm_semiring.mul_pos {α : Type u} {a b : α} :
0 < a * b 0 < a 0 < b
theorem mul_sub' {α : Type u} [has_sub α] (a b c : α) :
a * (b - c) = a * b - a * c
theorem sub_mul' {α : Type u} [has_sub α] (a b c : α) :
(a - b) * c = a * c - b * c

### Structures involving `*` and `0` on `with_top` and `with_bot`#

The main results of this section are `with_top.canonically_ordered_comm_semiring` and `with_bot.comm_monoid_with_zero`.

@[instance]
def with_top.nontrivial {α : Type u} [nonempty α] :
@[instance]
def with_top.mul_zero_class {α : Type u} [decidable_eq α] [has_zero α] [has_mul α] :
Equations
theorem with_top.mul_def {α : Type u} [decidable_eq α] [has_zero α] [has_mul α] {a b : with_top α} :
a * b = ite (a = 0 b = 0) 0 (λ (a : α), (λ (b : α), a * b)))
@[simp]
theorem with_top.mul_top {α : Type u} [decidable_eq α] [has_zero α] [has_mul α] {a : with_top α} (h : a 0) :
@[simp]
theorem with_top.top_mul {α : Type u} [decidable_eq α] [has_zero α] [has_mul α] {a : with_top α} (h : a 0) :
@[simp]
theorem with_top.top_mul_top {α : Type u} [decidable_eq α] [has_zero α] [has_mul α] :
theorem with_top.coe_mul {α : Type u} [decidable_eq α] {a b : α} :
a * b = (a) * b
theorem with_top.mul_coe {α : Type u} [decidable_eq α] {b : α} (hb : b 0) {a : with_top α} :
a * b = (λ (a : α), a * b)
@[simp]
theorem with_top.mul_eq_top_iff {α : Type u} [decidable_eq α] {a b : with_top α} :
a * b = a 0 b = a = b 0
theorem with_top.mul_lt_top {α : Type u} [decidable_eq α] {a b : with_top α} (ha : a < ) (hb : b < ) :
a * b <
@[instance]
def with_top.mul_zero_one_class {α : Type u} [decidable_eq α] [nontrivial α] :

`nontrivial α` is needed here as otherwise we have `1 * ⊤ = ⊤` but also `= 0 * ⊤ = 0`.

Equations
@[instance]
def with_top.no_zero_divisors {α : Type u} [decidable_eq α]  :
@[instance]
def with_top.semigroup_with_zero {α : Type u} [decidable_eq α]  :
Equations
@[instance]
def with_top.monoid_with_zero {α : Type u} [decidable_eq α] [nontrivial α] :
Equations
@[instance]
def with_top.comm_monoid_with_zero {α : Type u} [decidable_eq α] [nontrivial α] :
Equations