mathlib documentation

algebra.ordered_ring

@[instance]
def ordered_semiring.to_semiring (α : Type u) [s : ordered_semiring α] :

@[class]
structure ordered_semiring  :
Type uType u
  • add : α → α → α
  • add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • add_comm : ∀ (a b : α), a + b = b + a
  • mul : α → α → α
  • mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • zero_mul : ∀ (a : α), 0 * a = 0
  • mul_zero : ∀ (a : α), a * 0 = 0
  • left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
  • right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
  • add_left_cancel : ∀ (a b c_1 : α), a + b = a + c_1b = c_1
  • add_right_cancel : ∀ (a b c_1 : α), a + b = c_1 + ba = c_1
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
  • 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_1 : α), c_1 + a c_1 + b
  • le_of_add_le_add_left : ∀ (a b c_1 : α), a + b a + c_1b c_1
  • zero_le_one : 0 1
  • mul_lt_mul_of_pos_left : ∀ (a b c_1 : α), a < b0 < c_1c_1 * a < c_1 * b
  • mul_lt_mul_of_pos_right : ∀ (a b c_1 : α), a < b0 < c_1a * c_1 < b * c_1

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

Instances
theorem zero_le_one {α : Type u} [ordered_semiring α] :
0 1

theorem zero_le_two {α : Type u} [ordered_semiring α] :
0 2

theorem zero_lt_one {α : Type u} [ordered_semiring α] [nontrivial α] :
0 < 1

theorem zero_lt_two {α : Type u} [ordered_semiring α] [nontrivial α] :
0 < 2

theorem two_ne_zero {α : Type u} [ordered_semiring α] [nontrivial α] :
2 0

theorem one_lt_two {α : Type u} [ordered_semiring α] [nontrivial α] :
1 < 2

theorem one_le_two {α : Type u} [ordered_semiring α] [nontrivial α] :
1 2

theorem zero_lt_three {α : Type u} [ordered_semiring α] [nontrivial α] :
0 < 3

theorem zero_lt_four {α : Type u} [ordered_semiring α] [nontrivial α] :
0 < 4

theorem mul_lt_mul_of_pos_left {α : Type u} [ordered_semiring α] {a b c : α} :
a < b0 < cc * a < c * b

theorem mul_lt_mul_of_pos_right {α : Type u} [ordered_semiring α] {a b c : α} :
a < b0 < ca * c < b * c

theorem mul_le_mul_of_nonneg_left {α : Type u} [ordered_semiring α] {a b c : α} :
a b0 cc * a c * b

theorem mul_le_mul_of_nonneg_right {α : Type u} [ordered_semiring α] {a b c : α} :
a b0 ca * c b * c

theorem mul_le_mul {α : Type u} [ordered_semiring α] {a b c d : α} :
a cb d0 b0 ca * b c * d

theorem mul_nonneg {α : Type u} [ordered_semiring α] {a b : α} :
0 a0 b0 a * b

theorem mul_nonpos_of_nonneg_of_nonpos {α : Type u} [ordered_semiring α] {a b : α} :
0 ab 0a * b 0

theorem mul_nonpos_of_nonpos_of_nonneg {α : Type u} [ordered_semiring α] {a b : α} :
a 00 ba * b 0

theorem mul_lt_mul {α : Type u} [ordered_semiring α] {a b c d : α} :
a < cb d0 < b0 ca * b < c * d

theorem mul_lt_mul' {α : Type u} [ordered_semiring α] {a b c d : α} :
a cb < d0 b0 < ca * b < c * d

theorem mul_pos {α : Type u} [ordered_semiring α] {a b : α} :
0 < a0 < b0 < a * b

theorem mul_neg_of_pos_of_neg {α : Type u} [ordered_semiring α] {a b : α} :
0 < ab < 0a * b < 0

theorem mul_neg_of_neg_of_pos {α : Type u} [ordered_semiring α] {a b : α} :
a < 00 < ba * b < 0

theorem mul_self_le_mul_self {α : Type u} [ordered_semiring α] {a b : α} :
0 aa ba * a b * b

theorem mul_self_lt_mul_self {α : Type u} [ordered_semiring α] {a b : α} :
0 aa < ba * a < b * b

theorem mul_lt_mul'' {α : Type u} [ordered_semiring α] {a b c d : α} :
a < cb < d0 a0 ba * b < c * d

theorem le_mul_of_one_le_right {α : Type u} [ordered_semiring α] {a b : α} :
0 b1 ab b * a

theorem le_mul_of_one_le_left {α : Type u} [ordered_semiring α] {a b : α} :
0 b1 ab a * b

theorem bit1_pos {α : Type u} [ordered_semiring α] {a : α} [nontrivial α] :
0 a0 < bit1 a

theorem lt_add_one {α : Type u} [ordered_semiring α] [nontrivial α] (a : α) :
a < a + 1

theorem lt_one_add {α : Type u} [ordered_semiring α] [nontrivial α] (a : α) :
a < 1 + a

theorem bit1_pos' {α : Type u} [ordered_semiring α] {a : α} :
0 < a0 < bit1 a

theorem one_lt_mul {α : Type u} [ordered_semiring α] {a b : α} :
1 a1 < b1 < a * b

theorem mul_le_one {α : Type u} [ordered_semiring α] {a b : α} :
a 10 bb 1a * b 1

theorem one_lt_mul_of_le_of_lt {α : Type u} [ordered_semiring α] {a b : α} :
1 a1 < b1 < a * b

theorem one_lt_mul_of_lt_of_le {α : Type u} [ordered_semiring α] {a b : α} :
1 < a1 b1 < a * b

theorem mul_le_of_le_one_right {α : Type u} [ordered_semiring α] {a b : α} :
0 ab 1a * b a

theorem mul_le_of_le_one_left {α : Type u} [ordered_semiring α] {a b : α} :
0 ba 1a * b b

theorem mul_lt_one_of_nonneg_of_lt_one_left {α : Type u} [ordered_semiring α] {a b : α} :
0 aa < 1b 1a * b < 1

theorem mul_lt_one_of_nonneg_of_lt_one_right {α : Type u} [ordered_semiring α] {a b : α} :
a 10 bb < 1a * b < 1

@[class]
structure linear_ordered_semiring  :
Type uType u
  • add : α → α → α
  • add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • add_comm : ∀ (a b : α), a + b = b + a
  • mul : α → α → α
  • mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • zero_mul : ∀ (a : α), 0 * a = 0
  • mul_zero : ∀ (a : α), a * 0 = 0
  • left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
  • right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
  • add_left_cancel : ∀ (a b c_1 : α), a + b = a + c_1b = c_1
  • add_right_cancel : ∀ (a b c_1 : α), a + b = c_1 + ba = c_1
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
  • 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_1 : α), c_1 + a c_1 + b
  • le_of_add_le_add_left : ∀ (a b c_1 : α), a + b a + c_1b c_1
  • zero_le_one : 0 1
  • mul_lt_mul_of_pos_left : ∀ (a b c_1 : α), a < b0 < c_1c_1 * a < c_1 * b
  • mul_lt_mul_of_pos_right : ∀ (a b c_1 : α), a < b0 < c_1a * c_1 < b * c_1
  • le_total : ∀ (a b : α), a b b a
  • decidable_le : decidable_rel has_le.le
  • decidable_eq : decidable_eq α
  • decidable_lt : decidable_rel has_lt.lt
  • exists_pair_ne : ∃ (x y : α), x y

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

Instances
theorem zero_lt_one' {α : Type u} [linear_ordered_semiring α] :
0 < 1

theorem lt_of_mul_lt_mul_left {α : Type u} [linear_ordered_semiring α] {a b c : α} :
c * a < c * b0 ca < b

theorem lt_of_mul_lt_mul_right {α : Type u} [linear_ordered_semiring α] {a b c : α} :
a * c < b * c0 ca < b

theorem le_of_mul_le_mul_left {α : Type u} [linear_ordered_semiring α] {a b c : α} :
c * a c * b0 < ca b

theorem le_of_mul_le_mul_right {α : Type u} [linear_ordered_semiring α] {a b c : α} :
a * c b * c0 < ca b

theorem pos_and_pos_or_neg_and_neg_of_mul_pos {α : Type u} [linear_ordered_semiring α] {a b : α} :
0 < a * b0 < a 0 < b a < 0 b < 0

theorem nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nnonneg {α : Type u} [linear_ordered_semiring α] {a b : α} :
0 a * b0 a 0 b a 0 b 0

theorem pos_of_mul_pos_left {α : Type u} [linear_ordered_semiring α] {a b : α} :
0 < a * b0 a0 < b

theorem pos_of_mul_pos_right {α : Type u} [linear_ordered_semiring α] {a b : α} :
0 < a * b0 b0 < a

theorem nonneg_of_mul_nonneg_left {α : Type u} [linear_ordered_semiring α] {a b : α} :
0 a * b0 < a0 b

theorem nonneg_of_mul_nonneg_right {α : Type u} [linear_ordered_semiring α] {a b : α} :
0 a * b0 < b0 a

theorem neg_of_mul_neg_left {α : Type u} [linear_ordered_semiring α] {a b : α} :
a * b < 00 ab < 0

theorem neg_of_mul_neg_right {α : Type u} [linear_ordered_semiring α] {a b : α} :
a * b < 00 ba < 0

theorem nonpos_of_mul_nonpos_left {α : Type u} [linear_ordered_semiring α] {a b : α} :
a * b 00 < ab 0

theorem nonpos_of_mul_nonpos_right {α : Type u} [linear_ordered_semiring α] {a b : α} :
a * b 00 < ba 0

@[simp]
theorem mul_le_mul_left {α : Type u} [linear_ordered_semiring α] {a b c : α} :
0 < c(c * a c * b a b)

@[simp]
theorem mul_le_mul_right {α : Type u} [linear_ordered_semiring α] {a b c : α} :
0 < c(a * c b * c a b)

@[simp]
theorem mul_lt_mul_left {α : Type u} [linear_ordered_semiring α] {a b c : α} :
0 < c(c * a < c * b a < b)

@[simp]
theorem mul_lt_mul_right {α : Type u} [linear_ordered_semiring α] {a b c : α} :
0 < c(a * c < b * c a < b)

@[simp]
theorem zero_le_mul_left {α : Type u} [linear_ordered_semiring α] {b c : α} :
0 < c(0 c * b 0 b)

@[simp]
theorem zero_le_mul_right {α : Type u} [linear_ordered_semiring α] {b c : α} :
0 < c(0 b * c 0 b)

@[simp]
theorem zero_lt_mul_left {α : Type u} [linear_ordered_semiring α] {b c : α} :
0 < c(0 < c * b 0 < b)

@[simp]
theorem zero_lt_mul_right {α : Type u} [linear_ordered_semiring α] {b c : α} :
0 < c(0 < b * c 0 < b)

@[simp]
theorem bit0_le_bit0 {α : Type u} [linear_ordered_semiring α] {a b : α} [nontrivial α] :
bit0 a bit0 b a b

@[simp]
theorem bit0_lt_bit0 {α : Type u} [linear_ordered_semiring α] {a b : α} [nontrivial α] :
bit0 a < bit0 b a < b

@[simp]
theorem bit1_le_bit1 {α : Type u} [linear_ordered_semiring α] {a b : α} [nontrivial α] :
bit1 a bit1 b a b

@[simp]
theorem bit1_lt_bit1 {α : Type u} [linear_ordered_semiring α] {a b : α} [nontrivial α] :
bit1 a < bit1 b a < b

@[simp]
theorem one_le_bit1 {α : Type u} [linear_ordered_semiring α] {a : α} [nontrivial α] :
1 bit1 a 0 a

@[simp]
theorem one_lt_bit1 {α : Type u} [linear_ordered_semiring α] {a : α} [nontrivial α] :
1 < bit1 a 0 < a

@[simp]
theorem zero_le_bit0 {α : Type u} [linear_ordered_semiring α] {a : α} [nontrivial α] :
0 bit0 a 0 a

@[simp]
theorem zero_lt_bit0 {α : Type u} [linear_ordered_semiring α] {a : α} [nontrivial α] :
0 < bit0 a 0 < a

theorem le_mul_iff_one_le_left {α : Type u} [linear_ordered_semiring α] {a b : α} :
0 < b(b a * b 1 a)

theorem lt_mul_iff_one_lt_left {α : Type u} [linear_ordered_semiring α] {a b : α} :
0 < b(b < a * b 1 < a)

theorem le_mul_iff_one_le_right {α : Type u} [linear_ordered_semiring α] {a b : α} :
0 < b(b b * a 1 a)

theorem lt_mul_iff_one_lt_right {α : Type u} [linear_ordered_semiring α] {a b : α} :
0 < b(b < b * a 1 < a)

theorem lt_mul_of_one_lt_right {α : Type u} [linear_ordered_semiring α] {a b : α} :
0 < b1 < ab < b * a

theorem mul_nonneg_iff_right_nonneg_of_pos {α : Type u} [linear_ordered_semiring α] {a b : α} :
0 < a(0 b * a 0 b)

theorem mul_le_iff_le_one_left {α : Type u} [linear_ordered_semiring α] {a b : α} :
0 < b(a * b b a 1)

theorem mul_lt_iff_lt_one_left {α : Type u} [linear_ordered_semiring α] {a b : α} :
0 < b(a * b < b a < 1)

theorem mul_le_iff_le_one_right {α : Type u} [linear_ordered_semiring α] {a b : α} :
0 < b(b * a b a 1)

theorem mul_lt_iff_lt_one_right {α : Type u} [linear_ordered_semiring α] {a b : α} :
0 < b(b * a < b a < 1)

theorem nonpos_of_mul_nonneg_left {α : Type u} [linear_ordered_semiring α] {a b : α} :
0 a * bb < 0a 0

theorem nonpos_of_mul_nonneg_right {α : Type u} [linear_ordered_semiring α] {a b : α} :
0 a * ba < 0b 0

theorem neg_of_mul_pos_left {α : Type u} [linear_ordered_semiring α] {a b : α} :
0 < a * bb 0a < 0

theorem neg_of_mul_pos_right {α : Type u} [linear_ordered_semiring α] {a b : α} :
0 < a * ba 0b < 0

theorem exists_lt_mul_self {α : Type u} [linear_ordered_semiring α] (a : α) :
∃ (x : α), a < x * x

theorem exists_le_mul_self {α : Type u} [linear_ordered_semiring α] (a : α) :
∃ (x : α), a x * x

theorem monotone_mul_left_of_nonneg {α : Type u} [linear_ordered_semiring α] {a : α} :
0 amonotone (λ (x : α), a * x)

theorem monotone_mul_right_of_nonneg {α : Type u} [linear_ordered_semiring α] {a : α} :
0 amonotone (λ (x : α), x * a)

theorem monotone.mul_const {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [preorder β] {f : β → α} {a : α} :
monotone f0 amonotone (λ (x : β), (f x) * a)

theorem monotone.const_mul {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [preorder β] {f : β → α} {a : α} :
monotone f0 amonotone (λ (x : β), a * f x)

theorem monotone.mul {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [preorder β] {f g : β → α} :
monotone fmonotone g(∀ (x : β), 0 f x)(∀ (x : β), 0 g x)monotone (λ (x : β), (f x) * g x)

theorem strict_mono_mul_left_of_pos {α : Type u} [linear_ordered_semiring α] {a : α} :
0 < astrict_mono (λ (x : α), a * x)

theorem strict_mono_mul_right_of_pos {α : Type u} [linear_ordered_semiring α] {a : α} :
0 < astrict_mono (λ (x : α), x * a)

theorem strict_mono.mul_const {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [preorder β] {f : β → α} {a : α} :
strict_mono f0 < astrict_mono (λ (x : β), (f x) * a)

theorem strict_mono.const_mul {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [preorder β] {f : β → α} {a : α} :
strict_mono f0 < astrict_mono (λ (x : β), a * f x)

theorem strict_mono.mul_monotone {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [preorder β] {f g : β → α} :
strict_mono fmonotone g(∀ (x : β), 0 f x)(∀ (x : β), 0 < g x)strict_mono (λ (x : β), (f x) * g x)

theorem monotone.mul_strict_mono {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [preorder β] {f g : β → α} :
monotone fstrict_mono g(∀ (x : β), 0 < f x)(∀ (x : β), 0 g x)strict_mono (λ (x : β), (f x) * g x)

theorem strict_mono.mul {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [preorder β] {f g : β → α} :
strict_mono fstrict_mono g(∀ (x : β), 0 f x)(∀ (x : β), 0 g x)strict_mono (λ (x : β), (f x) * g x)

@[simp]
theorem decidable.mul_le_mul_left {α : Type u} [linear_ordered_semiring α] {a b c : α} :
0 < c(c * a c * b a b)

@[simp]
theorem decidable.mul_le_mul_right {α : Type u} [linear_ordered_semiring α] {a b c : α} :
0 < c(a * c b * c a b)

theorem mul_max_of_nonneg {α : Type u} [linear_ordered_semiring α] {a : α} (b c : α) :
0 aa * max b c = max (a * b) (a * c)

theorem mul_min_of_nonneg {α : Type u} [linear_ordered_semiring α] {a : α} (b c : α) :
0 aa * min b c = min (a * b) (a * c)

theorem max_mul_of_nonneg {α : Type u} [linear_ordered_semiring α] {c : α} (a b : α) :
0 c(max a b) * c = max (a * c) (b * c)

theorem min_mul_of_nonneg {α : Type u} [linear_ordered_semiring α] {c : α} (a b : α) :
0 c(min a b) * c = min (a * c) (b * c)

@[class]
structure ordered_ring  :
Type uType u
  • add : α → α → α
  • add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • neg : α → α
  • add_left_neg : ∀ (a : α), -a + a = 0
  • add_comm : ∀ (a b : α), a + b = b + a
  • mul : α → α → α
  • mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
  • right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
  • 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_1 : α), c_1 + a c_1 + 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 multiplication with a positive number and addition are monotone.

Instances
@[instance]
def ordered_ring.to_ring (α : Type u) [s : ordered_ring α] :
ring α

theorem ordered_ring.mul_nonneg {α : Type u} [ordered_ring α] (a b : α) :
0 a0 b0 a * b

theorem ordered_ring.mul_le_mul_of_nonneg_left {α : Type u} [ordered_ring α] {a b c : α} :
a b0 cc * a c * b

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 : α} :
a < b0 < cc * a < c * b

theorem ordered_ring.mul_lt_mul_of_pos_right {α : Type u} [ordered_ring α] {a b c : α} :
a < b0 < ca * c < b * c

theorem mul_le_mul_of_nonpos_left {α : Type u} [ordered_ring α] {a b c : α} :
b ac 0c * a c * b

theorem mul_le_mul_of_nonpos_right {α : Type u} [ordered_ring α] {a b c : α} :
b ac 0a * c b * c

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 : α} :
b < ac < 0c * a < c * b

theorem mul_lt_mul_of_neg_right {α : Type u} [ordered_ring α] {a b c : α} :
b < ac < 0a * c < b * c

theorem mul_pos_of_neg_of_neg {α : Type u} [ordered_ring α] {a b : α} :
a < 0b < 00 < a * b

@[instance]

@[instance]

@[class]
structure linear_ordered_ring  :
Type uType u
  • add : α → α → α
  • add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • neg : α → α
  • add_left_neg : ∀ (a : α), -a + a = 0
  • add_comm : ∀ (a b : α), a + b = b + a
  • mul : α → α → α
  • mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
  • right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
  • 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_1 : α), c_1 + a c_1 + 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_rel has_le.le
  • decidable_eq : decidable_eq α
  • decidable_lt : decidable_rel has_lt.lt
  • exists_pair_ne : ∃ (x y : α), x y

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

Instances
@[instance]

@[simp]
theorem abs_one {α : Type u} [linear_ordered_ring α] :
abs 1 = 1

@[simp]
theorem abs_two {α : Type u} [linear_ordered_ring α] :
abs 2 = 2

theorem abs_mul {α : Type u} [linear_ordered_ring α] (a b : α) :
abs (a * b) = (abs a) * abs b

theorem abs_mul_abs_self {α : Type u} [linear_ordered_ring α] (a : α) :
(abs a) * abs a = a * a

theorem abs_mul_self {α : Type u} [linear_ordered_ring α] (a : α) :
abs (a * a) = a * a

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_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

theorem gt_of_mul_lt_mul_neg_left {α : Type u} [linear_ordered_ring α] {a b c : α} :
c * a < c * bc 0b < a

theorem neg_one_lt_zero {α : Type u} [linear_ordered_ring α] :
-1 < 0

theorem le_of_mul_le_of_one_le {α : Type u} [linear_ordered_ring α] {a b c : α} :
a * c b0 b1 ca b

theorem nonneg_le_nonneg_of_squares_le {α : Type u} [linear_ordered_ring α] {a b : α} :
0 ba * a b * ba b

theorem mul_self_le_mul_self_iff {α : Type u} [linear_ordered_ring α] {a b : α} :
0 a0 b(a b a * a b * b)

theorem mul_self_lt_mul_self_iff {α : Type u} [linear_ordered_ring α] {a b : α} :
0 a0 b(a < b a * a < b * b)

theorem mul_self_inj {α : Type u} [linear_ordered_ring α] {a b : α} :
0 a0 b(a * a = b * b a = b)

@[simp]
theorem mul_le_mul_left_of_neg {α : Type u} [linear_ordered_ring α] {a b c : α} :
c < 0(c * a c * b b a)

@[simp]
theorem mul_le_mul_right_of_neg {α : Type u} [linear_ordered_ring α] {a b c : α} :
c < 0(a * c b * c b a)

@[simp]
theorem mul_lt_mul_left_of_neg {α : Type u} [linear_ordered_ring α] {a b c : α} :
c < 0(c * a < c * b b < a)

@[simp]
theorem mul_lt_mul_right_of_neg {α : Type u} [linear_ordered_ring α] {a b c : α} :
c < 0(a * c < b * c b < a)

theorem sub_one_lt {α : Type u} [linear_ordered_ring α] (a : α) :
a - 1 < a

theorem mul_self_pos {α : Type u} [linear_ordered_ring α] {a : α} :
a 00 < a * a

theorem mul_self_le_mul_self_of_le_of_neg_le {α : Type u} [linear_ordered_ring α] {x y : α} :
x y-x yx * x y * y

theorem nonneg_of_mul_nonpos_left {α : Type u} [linear_ordered_ring α] {a b : α} :
a * b 0b < 00 a

theorem nonneg_of_mul_nonpos_right {α : Type u} [linear_ordered_ring α] {a b : α} :
a * b 0a < 00 b

theorem pos_of_mul_neg_left {α : Type u} [linear_ordered_ring α] {a b : α} :
a * b < 0b 00 < a

theorem pos_of_mul_neg_right {α : Type u} [linear_ordered_ring α] {a b : α} :
a * b < 0a 00 < b

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 sub_le_of_abs_sub_le_left {α : Type u} [linear_ordered_ring α] {a b c : α} :
abs (a - b) cb - c a

theorem sub_le_of_abs_sub_le_right {α : Type u} [linear_ordered_ring α] {a b c : α} :
abs (a - b) ca - c b

theorem sub_lt_of_abs_sub_lt_left {α : Type u} [linear_ordered_ring α] {a b c : α} :
abs (a - b) < cb - c < a

theorem sub_lt_of_abs_sub_lt_right {α : Type u} [linear_ordered_ring α] {a b c : α} :
abs (a - b) < ca - c < b

theorem eq_zero_of_mul_self_add_mul_self_eq_zero {α : Type u} [linear_ordered_ring α] {a b : α} :
a * a + b * b = 0a = 0

theorem abs_eq_iff_mul_self_eq {α : Type u} [linear_ordered_ring α] {a b : α} :
abs a = abs b a * a = b * b

theorem abs_lt_iff_mul_self_lt {α : Type u} [linear_ordered_ring α] {a b : α} :
abs a < abs b a * a < b * b

theorem abs_le_iff_mul_self_le {α : Type u} [linear_ordered_ring α] {a b : α} :
abs a abs b a * a b * b

@[class]
structure linear_ordered_comm_ring  :
Type uType u
  • add : α → α → α
  • add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • neg : α → α
  • add_left_neg : ∀ (a : α), -a + a = 0
  • add_comm : ∀ (a b : α), a + b = b + a
  • mul : α → α → α
  • mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
  • right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
  • 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_1 : α), c_1 + a c_1 + 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_rel has_le.le
  • decidable_eq : decidable_eq α
  • decidable_lt : decidable_rel has_lt.lt
  • 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 multiplication with a positive number and addition are monotone.

Instances
theorem max_mul_mul_le_max_mul_max {α : Type u} [linear_ordered_comm_ring α] {a d : α} (b c : α) :
0 a0 dmax (a * b) (d * c) (max a c) * max d b

theorem abs_sub_square {α : Type u} [linear_ordered_comm_ring α] (a b : α) :
(abs (a - b)) * abs (a - b) = a * a + b * b - ((1 + 1) * a) * b

@[instance]
def nonneg_ring.to_ring (α : Type u_1) [s : nonneg_ring α] :
ring α

@[class]
structure nonneg_ring  :
Type u_1Type u_1

Extend nonneg_add_comm_group to support ordered rings specified by their nonnegative elements

Instances
@[instance]

@[class]
structure linear_nonneg_ring  :
Type u_1Type u_1

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) [s : linear_nonneg_ring α] :

to_linear_nonneg_ring shows that a nonneg_ring with a total 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

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_1Type u_1
  • add : α → α → α
  • add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • add_comm : ∀ (a b : α), a + b = b + a
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
  • 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_1 : α), c_1 + a c_1 + b
  • lt_of_add_lt_add_left : ∀ (a b c_1 : α), a + b < a + c_1b < c_1
  • bot : α
  • bot_le : ∀ (a : α), a
  • le_iff_exists_add : ∀ (a b : α), a b ∃ (c_1 : α), b = a + c_1
  • mul : α → α → α
  • mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • zero_mul : ∀ (a : α), 0 * a = 0
  • mul_zero : ∀ (a : α), a * 0 = 0
  • left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
  • right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
  • 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
theorem canonically_ordered_semiring.mul_le_mul {α : Type u} [canonically_ordered_comm_semiring α] {a b c d : α} :
a bc da * c b * d

theorem canonically_ordered_semiring.mul_le_mul_left' {α : Type u} [canonically_ordered_comm_semiring α] {b c : α} (h : b c) (a : α) :
a * b a * c

theorem canonically_ordered_semiring.mul_le_mul_right' {α : Type u} [canonically_ordered_comm_semiring α] {b c : α} (h : b c) (a : α) :
b * a c * a

theorem canonically_ordered_semiring.mul_pos {α : Type u} [canonically_ordered_comm_semiring α] {a b : α} :
0 < a * b 0 < a 0 < b

@[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 (option.bind a (λ (a : α), option.bind b (λ (b : α), a * b)))

@[simp]
theorem with_top.mul_top {α : Type u} [decidable_eq α] [has_zero α] [has_mul α] {a : with_top α} :
a 0a * =

@[simp]
theorem with_top.top_mul {α : Type u} [decidable_eq α] [has_zero α] [has_mul α] {a : with_top α} :
a 0 * a =

@[simp]
theorem with_top.top_mul_top {α : Type u} [decidable_eq α] [has_zero α] [has_mul α] :

theorem with_top.coe_mul {α : Type u} [decidable_eq α] [mul_zero_class α] {a b : α} :
a * b = (a) * b

theorem with_top.mul_coe {α : Type u} [decidable_eq α] [mul_zero_class α] {b : α} (hb : b 0) {a : with_top α} :
a * b = option.bind a (λ (a : α), a * b)

@[simp]
theorem with_top.mul_eq_top_iff {α : Type u} [decidable_eq α] [mul_zero_class α] {a b : with_top α} :
a * b = a 0 b = a = b 0