mathlib documentation

algebra.ordered_ring

source
@[instance]
def ordered_semiring.to_semiring (α : Type u) [self : ordered_semiring α] :
semiring α
source
@[class]
structure ordered_semiring (α : Type u) :
Type 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
  • nsmul : ℕ → α → α
  • nsmul_zero' : (∀ (x : α), ordered_semiring.nsmul 0 x = 0) . "try_refl_tac"
  • nsmul_succ' : (∀ (n : ℕ) (x : α), ordered_semiring.nsmul n.succ x = x + ordered_semiring.nsmul n x) . "try_refl_tac"
  • 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
  • npow : ℕ → α → α
  • npow_zero' : (∀ (x : α), ordered_semiring.npow 0 x = 1) . "try_refl_tac"
  • npow_succ' : (∀ (n : ℕ) (x : α), ordered_semiring.npow n.succ x = x * ordered_semiring.npow n x) . "try_refl_tac"
  • 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_1 → b = c_1
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = 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_1 → b ≤ c_1
  • zero_le_one : 0 ≤ 1
  • mul_lt_mul_of_pos_left : ∀ (a b c_1 : α), a < b → 0 < c_1 → c_1 * a < c_1 * b
  • mul_lt_mul_of_pos_right : ∀ (a b c_1 : α), a < b → 0 < c_1 → a * 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
source
@[instance]
def ordered_semiring.to_ordered_cancel_add_comm_monoid (α : Type u) [self : ordered_semiring α] :
ordered_cancel_add_comm_monoid α
source
theorem zero_le_one {α : Type u} [ordered_semiring α] :
0 ≤ 1
source
theorem zero_le_two {α : Type u} [ordered_semiring α] :
0 ≤ 2
source
theorem one_le_two {α : Type u} [ordered_semiring α] :
1 ≤ 2
source
theorem zero_lt_one {α : Type u} [ordered_semiring α] [nontrivial α] :
0 < 1
source
theorem zero_lt_two {α : Type u} [ordered_semiring α] [nontrivial α] :
0 < 2
source
theorem two_ne_zero {α : Type u} [ordered_semiring α] [nontrivial α] :
2 ≠ 0
source
theorem one_lt_two {α : Type u} [ordered_semiring α] [nontrivial α] :
1 < 2
source
theorem zero_lt_three {α : Type u} [ordered_semiring α] [nontrivial α] :
0 < 3
source
theorem zero_lt_four {α : Type u} [ordered_semiring α] [nontrivial α] :
0 < 4
source
theorem mul_lt_mul_of_pos_left {α : Type u} [ordered_semiring α] {a b c : α} (h₁ : a < b) (h₂ : 0 < c) :
c * a < c * b
source
theorem mul_lt_mul_of_pos_right {α : Type u} [ordered_semiring α] {a b c : α} (h₁ : a < b) (h₂ : 0 < c) :
a * c < b * c
source
@[protected]
theorem decidable.mul_le_mul_of_nonneg_left {α : Type u} [ordered_semiring α] {a b c : α} [decidable_rel has_le.le] (h₁ : a ≤ b) (h₂ : 0 ≤ c) :
c * a ≤ c * b
source
theorem mul_le_mul_of_nonneg_left {α : Type u} [ordered_semiring α] {a b c : α} :
a ≤ b → 0 ≤ c → c * a ≤ c * b
source
@[protected]
theorem decidable.mul_le_mul_of_nonneg_right {α : Type u} [ordered_semiring α] {a b c : α} [decidable_rel has_le.le] (h₁ : a ≤ b) (h₂ : 0 ≤ c) :
a * c ≤ b * c
source
theorem mul_le_mul_of_nonneg_right {α : Type u} [ordered_semiring α] {a b c : α} :
a ≤ b → 0 ≤ c → a * c ≤ b * c
source
@[protected]
theorem decidable.mul_le_mul {α : Type u} [ordered_semiring α] {a b c d : α} [decidable_rel has_le.le] (hac : a ≤ c) (hbd : b ≤ d) (nn_b : 0 ≤ b) (nn_c : 0 ≤ c) :
a * b ≤ c * d
source
theorem mul_le_mul {α : Type u} [ordered_semiring α] {a b c d : α} :
a ≤ c → b ≤ d → 0 ≤ b → 0 ≤ c → a * b ≤ c * d
source
@[protected]
theorem decidable.mul_nonneg_le_one_le {α : Type u_1} [ordered_semiring α] [decidable_rel has_le.le] {a b c : α} (h₁ : 0 ≤ c) (h₂ : a ≤ c) (h₃ : 0 ≤ b) (h₄ : b ≤ 1) :
a * b ≤ c
source
theorem mul_nonneg_le_one_le {α : Type u_1} [ordered_semiring α] {a b c : α} :
0 ≤ c → a ≤ c → 0 ≤ b → b ≤ 1 → a * b ≤ c
source
@[protected]
theorem decidable.mul_nonneg {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (ha : 0 ≤ a) (hb : 0 ≤ b) :
0 ≤ a * b
source
theorem mul_nonneg {α : Type u} [ordered_semiring α] {a b : α} :
0 ≤ a → 0 ≤ b → 0 ≤ a * b
source
@[protected]
theorem decidable.mul_nonpos_of_nonneg_of_nonpos {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (ha : 0 ≤ a) (hb : b ≤ 0) :
a * b ≤ 0
source
theorem mul_nonpos_of_nonneg_of_nonpos {α : Type u} [ordered_semiring α] {a b : α} :
0 ≤ a → b ≤ 0 → a * b ≤ 0
source
@[protected]
theorem decidable.mul_nonpos_of_nonpos_of_nonneg {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (ha : a ≤ 0) (hb : 0 ≤ b) :
a * b ≤ 0
source
theorem mul_nonpos_of_nonpos_of_nonneg {α : Type u} [ordered_semiring α] {a b : α} :
a ≤ 0 → 0 ≤ b → a * b ≤ 0
source
@[protected]
theorem decidable.mul_lt_mul {α : Type u} [ordered_semiring α] {a b c d : α} [decidable_rel has_le.le] (hac : a < c) (hbd : b ≤ d) (pos_b : 0 < b) (nn_c : 0 ≤ c) :
a * b < c * d
source
theorem mul_lt_mul {α : Type u} [ordered_semiring α] {a b c d : α} :
a < c → b ≤ d → 0 < b → 0 ≤ c → a * b < c * d
source
@[protected]
theorem decidable.mul_lt_mul' {α : Type u} [ordered_semiring α] {a b c d : α} [decidable_rel has_le.le] (h1 : a ≤ c) (h2 : b < d) (h3 : 0 ≤ b) (h4 : 0 < c) :
a * b < c * d
source
theorem mul_lt_mul' {α : Type u} [ordered_semiring α] {a b c d : α} :
a ≤ c → b < d → 0 ≤ b → 0 < c → a * b < c * d
source
theorem mul_pos {α : Type u} [ordered_semiring α] {a b : α} (ha : 0 < a) (hb : 0 < b) :
0 < a * b
source
theorem mul_neg_of_pos_of_neg {α : Type u} [ordered_semiring α] {a b : α} (ha : 0 < a) (hb : b < 0) :
a * b < 0
source
theorem mul_neg_of_neg_of_pos {α : Type u} [ordered_semiring α] {a b : α} (ha : a < 0) (hb : 0 < b) :
a * b < 0
source
@[protected]
theorem decidable.mul_self_lt_mul_self {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (h1 : 0 ≤ a) (h2 : a < b) :
a * a < b * b
source
theorem mul_self_lt_mul_self {α : Type u} [ordered_semiring α] {a b : α} (h1 : 0 ≤ a) (h2 : a < b) :
a * a < b * b
source
@[protected]
theorem decidable.strict_mono_incr_on_mul_self {α : Type u} [ordered_semiring α] [decidable_rel has_le.le] :
strict_mono_incr_on (λ (x : α), x * x) (set.Ici 0)
source
theorem strict_mono_incr_on_mul_self {α : Type u} [ordered_semiring α] :
strict_mono_incr_on (λ (x : α), x * x) (set.Ici 0)
source
@[protected]
theorem decidable.mul_self_le_mul_self {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (h1 : 0 ≤ a) (h2 : a ≤ b) :
a * a ≤ b * b
source
theorem mul_self_le_mul_self {α : Type u} [ordered_semiring α] {a b : α} (h1 : 0 ≤ a) (h2 : a ≤ b) :
a * a ≤ b * b
source
@[protected]
theorem decidable.mul_lt_mul'' {α : Type u} [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
source
theorem mul_lt_mul'' {α : Type u} [ordered_semiring α] {a b c d : α} :
a < c → b < d → 0 ≤ a → 0 ≤ b → a * b < c * d
source
@[protected]
theorem decidable.le_mul_of_one_le_right {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (hb : 0 ≤ b) (h : 1 ≤ a) :
b ≤ b * a
source
theorem le_mul_of_one_le_right {α : Type u} [ordered_semiring α] {a b : α} :
0 ≤ b → 1 ≤ a → b ≤ b * a
source
@[protected]
theorem decidable.le_mul_of_one_le_left {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (hb : 0 ≤ b) (h : 1 ≤ a) :
b ≤ a * b
source
theorem le_mul_of_one_le_left {α : Type u} [ordered_semiring α] {a b : α} :
0 ≤ b → 1 ≤ a → b ≤ a * b
source
@[protected]
theorem decidable.lt_mul_of_one_lt_right {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (hb : 0 < b) (h : 1 < a) :
b < b * a
source
theorem lt_mul_of_one_lt_right {α : Type u} [ordered_semiring α] {a b : α} :
0 < b → 1 < a → b < b * a
source
@[protected]
theorem decidable.lt_mul_of_one_lt_left {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (hb : 0 < b) (h : 1 < a) :
b < a * b
source
theorem lt_mul_of_one_lt_left {α : Type u} [ordered_semiring α] {a b : α} :
0 < b → 1 < a → b < a * b
source
@[protected]
theorem decidable.add_le_mul_two_add {α : Type u} [ordered_semiring α] [decidable_rel has_le.le] {a b : α} (a2 : 2 ≤ a) (b0 : 0 ≤ b) :
a + (2 + b) ≤ a * (2 + b)
source
theorem add_le_mul_two_add {α : Type u} [ordered_semiring α] {a b : α} :
2 ≤ a → 0 ≤ b → a + (2 + b) ≤ a * (2 + b)
source
@[protected]
theorem decidable.one_le_mul_of_one_le_of_one_le {α : Type u} [ordered_semiring α] [decidable_rel has_le.le] {a b : α} (a1 : 1 ≤ a) (b1 : 1 ≤ b) :
1 ≤ a * b
source
theorem one_le_mul_of_one_le_of_one_le {α : Type u} [ordered_semiring α] {a b : α} :
1 ≤ a → 1 ≤ b → 1 ≤ a * b
source
def function.injective.ordered_semiring {α : Type u} [ordered_semiring α] {β : 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) :
ordered_semiring β

Pullback an ordered_semiring under an injective map.

Equations
source
theorem bit1_pos {α : Type u} [ordered_semiring α] {a : α} [nontrivial α] (h : 0 ≤ a) :
0 < bit1 a
source
theorem lt_add_one {α : Type u} [ordered_semiring α] [nontrivial α] (a : α) :
a < a + 1
source
theorem lt_one_add {α : Type u} [ordered_semiring α] [nontrivial α] (a : α) :
a < 1 + a
source
theorem bit1_pos' {α : Type u} [ordered_semiring α] {a : α} (h : 0 < a) :
0 < bit1 a
source
@[protected]
theorem decidable.one_lt_mul {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (ha : 1 ≤ a) (hb : 1 < b) :
1 < a * b
source
theorem one_lt_mul {α : Type u} [ordered_semiring α] {a b : α} :
1 ≤ a → 1 < b → 1 < a * b
source
@[protected]
theorem decidable.mul_le_one {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (ha : a ≤ 1) (hb' : 0 ≤ b) (hb : b ≤ 1) :
a * b ≤ 1
source
theorem mul_le_one {α : Type u} [ordered_semiring α] {a b : α} :
a ≤ 1 → 0 ≤ b → b ≤ 1 → a * b ≤ 1
source
@[protected]
theorem decidable.one_lt_mul_of_le_of_lt {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (ha : 1 ≤ a) (hb : 1 < b) :
1 < a * b
source
theorem one_lt_mul_of_le_of_lt {α : Type u} [ordered_semiring α] {a b : α} :
1 ≤ a → 1 < b → 1 < a * b
source
@[protected]
theorem decidable.one_lt_mul_of_lt_of_le {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (ha : 1 < a) (hb : 1 ≤ b) :
1 < a * b
source
theorem one_lt_mul_of_lt_of_le {α : Type u} [ordered_semiring α] {a b : α} :
1 < a → 1 ≤ b → 1 < a * b
source
@[protected]
theorem decidable.mul_le_of_le_one_right {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (ha : 0 ≤ a) (hb1 : b ≤ 1) :
a * b ≤ a
source
theorem mul_le_of_le_one_right {α : Type u} [ordered_semiring α] {a b : α} :
0 ≤ a → b ≤ 1 → a * b ≤ a
source
@[protected]
theorem decidable.mul_le_of_le_one_left {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (hb : 0 ≤ b) (ha1 : a ≤ 1) :
a * b ≤ b
source
theorem mul_le_of_le_one_left {α : Type u} [ordered_semiring α] {a b : α} :
0 ≤ b → a ≤ 1 → a * b ≤ b
source
@[protected]
theorem decidable.mul_lt_one_of_nonneg_of_lt_one_left {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (ha0 : 0 ≤ a) (ha : a < 1) (hb : b ≤ 1) :
a * b < 1
source
theorem mul_lt_one_of_nonneg_of_lt_one_left {α : Type u} [ordered_semiring α] {a b : α} :
0 ≤ a → a < 1 → b ≤ 1 → a * b < 1
source
@[protected]
theorem decidable.mul_lt_one_of_nonneg_of_lt_one_right {α : Type u} [ordered_semiring α] {a b : α} [decidable_rel has_le.le] (ha : a ≤ 1) (hb0 : 0 ≤ b) (hb : b < 1) :
a * b < 1
source
theorem mul_lt_one_of_nonneg_of_lt_one_right {α : Type u} [ordered_semiring α] {a b : α} :
a ≤ 1 → 0 ≤ b → b < 1 → a * b < 1
source
@[instance]
def ordered_comm_semiring.to_comm_semiring (α : Type u) [self : ordered_comm_semiring α] :
comm_semiring α
source
@[instance]
def ordered_comm_semiring.to_ordered_semiring (α : Type u) [self : ordered_comm_semiring α] :
ordered_semiring α
source
@[class]
structure ordered_comm_semiring (α : Type u) :
Type 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
  • nsmul : ℕ → α → α
  • nsmul_zero' : (∀ (x : α), ordered_comm_semiring.nsmul 0 x = 0) . "try_refl_tac"
  • nsmul_succ' : (∀ (n : ℕ) (x : α), ordered_comm_semiring.nsmul n.succ x = x + ordered_comm_semiring.nsmul n x) . "try_refl_tac"
  • 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
  • npow : ℕ → α → α
  • npow_zero' : (∀ (x : α), ordered_comm_semiring.npow 0 x = 1) . "try_refl_tac"
  • npow_succ' : (∀ (n : ℕ) (x : α), ordered_comm_semiring.npow n.succ x = x * ordered_comm_semiring.npow n x) . "try_refl_tac"
  • 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_1 → b = c_1
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = 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_1 → b ≤ c_1
  • zero_le_one : 0 ≤ 1
  • mul_lt_mul_of_pos_left : ∀ (a b c_1 : α), a < b → 0 < c_1 → c_1 * a < c_1 * b
  • mul_lt_mul_of_pos_right : ∀ (a b c_1 : α), a < b → 0 < c_1 → a * c_1 < b * c_1
  • mul_comm : ∀ (a b : α), a * b = b * a

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

Instances
source
def function.injective.ordered_comm_semiring {α : Type u} [ordered_comm_semiring α] {β : 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) :
ordered_comm_semiring β

Pullback an ordered_comm_semiring under an injective map.

Equations
source
@[instance]
def linear_ordered_semiring.to_ordered_semiring (α : Type u) [self : linear_ordered_semiring α] :
ordered_semiring α
source
@[class]
structure linear_ordered_semiring (α : Type u) :
Type 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
  • nsmul : ℕ → α → α
  • nsmul_zero' : (∀ (x : α), linear_ordered_semiring.nsmul 0 x = 0) . "try_refl_tac"
  • nsmul_succ' : (∀ (n : ℕ) (x : α), linear_ordered_semiring.nsmul n.succ x = x + linear_ordered_semiring.nsmul n x) . "try_refl_tac"
  • 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
  • npow : ℕ → α → α
  • npow_zero' : (∀ (x : α), linear_ordered_semiring.npow 0 x = 1) . "try_refl_tac"
  • npow_succ' : (∀ (n : ℕ) (x : α), linear_ordered_semiring.npow n.succ x = x * linear_ordered_semiring.npow n x) . "try_refl_tac"
  • 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_1 → b = c_1
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = 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_1 → b ≤ c_1
  • zero_le_one : 0 ≤ 1
  • mul_lt_mul_of_pos_left : ∀ (a b c_1 : α), a < b → 0 < c_1 → c_1 * a < c_1 * b
  • mul_lt_mul_of_pos_right : ∀ (a b c_1 : α), a < b → 0 < c_1 → a * 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
source
@[instance]
def linear_ordered_semiring.to_linear_order (α : Type u) [self : linear_ordered_semiring α] :
linear_order α
source
@[instance]
def linear_ordered_semiring.to_nontrivial (α : Type u) [self : linear_ordered_semiring α] :
nontrivial α
source
theorem zero_lt_one' {α : Type u} [linear_ordered_semiring α] :
0 < 1
source
theorem lt_of_mul_lt_mul_left {α : Type u} [linear_ordered_semiring α] {a b c : α} (h : c * a < c * b) (hc : 0 ≤ c) :
a < b
source
theorem lt_of_mul_lt_mul_right {α : Type u} [linear_ordered_semiring α] {a b c : α} (h : a * c < b * c) (hc : 0 ≤ c) :
a < b
source
theorem le_of_mul_le_mul_left {α : Type u} [linear_ordered_semiring α] {a b c : α} (h : c * a ≤ c * b) (hc : 0 < c) :
a ≤ b
source
theorem le_of_mul_le_mul_right {α : Type u} [linear_ordered_semiring α] {a b c : α} (h : a * c ≤ b * c) (hc : 0 < c) :
a ≤ b
source
theorem pos_and_pos_or_neg_and_neg_of_mul_pos {α : Type u} [linear_ordered_semiring α] {a b : α} (hab : 0 < a * b) :
0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
source
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
source
theorem pos_of_mul_pos_left {α : Type u} [linear_ordered_semiring α] {a b : α} (h : 0 < a * b) (ha : 0 ≤ a) :
0 < b
source
theorem pos_of_mul_pos_right {α : Type u} [linear_ordered_semiring α] {a b : α} (h : 0 < a * b) (hb : 0 ≤ b) :
0 < a
source
@[simp]
theorem inv_of_pos {α : Type u} [linear_ordered_semiring α] {a : α} [invertible a] :
0 < ⅟ a ↔ 0 < a
source
@[simp]
theorem inv_of_nonpos {α : Type u} [linear_ordered_semiring α] {a : α} [invertible a] :
⅟ a ≤ 0 ↔ a ≤ 0
source
theorem nonneg_of_mul_nonneg_left {α : Type u} [linear_ordered_semiring α] {a b : α} (h : 0 ≤ a * b) (h1 : 0 < a) :
0 ≤ b
source
theorem nonneg_of_mul_nonneg_right {α : Type u} [linear_ordered_semiring α] {a b : α} (h : 0 ≤ a * b) (h1 : 0 < b) :
0 ≤ a
source
@[simp]
theorem inv_of_nonneg {α : Type u} [linear_ordered_semiring α] {a : α} [invertible a] :
0 ≤ ⅟ a ↔ 0 ≤ a
source
@[simp]
theorem inv_of_lt_zero {α : Type u} [linear_ordered_semiring α] {a : α} [invertible a] :
⅟ a < 0 ↔ a < 0
source
@[simp]
theorem inv_of_le_one {α : Type u} [linear_ordered_semiring α] {a : α} [invertible a] (h : 1 ≤ a) :
⅟ a ≤ 1
source
theorem neg_of_mul_neg_left {α : Type u} [linear_ordered_semiring α] {a b : α} (h : a * b < 0) (h1 : 0 ≤ a) :
b < 0
source
theorem neg_of_mul_neg_right {α : Type u} [linear_ordered_semiring α] {a b : α} (h : a * b < 0) (h1 : 0 ≤ b) :
a < 0
source
theorem nonpos_of_mul_nonpos_left {α : Type u} [linear_ordered_semiring α] {a b : α} (h : a * b ≤ 0) (h1 : 0 < a) :
b ≤ 0
source
theorem nonpos_of_mul_nonpos_right {α : Type u} [linear_ordered_semiring α] {a b : α} (h : a * b ≤ 0) (h1 : 0 < b) :
a ≤ 0
source
@[simp]
theorem mul_le_mul_left {α : Type u} [linear_ordered_semiring α] {a b c : α} (h : 0 < c) :
c * a ≤ c * b ↔ a ≤ b
source
@[simp]
theorem mul_le_mul_right {α : Type u} [linear_ordered_semiring α] {a b c : α} (h : 0 < c) :
a * c ≤ b * c ↔ a ≤ b
source
@[simp]
theorem mul_lt_mul_left {α : Type u} [linear_ordered_semiring α] {a b c : α} (h : 0 < c) :
c * a < c * b ↔ a < b
source
@[simp]
theorem mul_lt_mul_right {α : Type u} [linear_ordered_semiring α] {a b c : α} (h : 0 < c) :
a * c < b * c ↔ a < b
source
@[simp]
theorem zero_le_mul_left {α : Type u} [linear_ordered_semiring α] {b c : α} (h : 0 < c) :
0 ≤ c * b ↔ 0 ≤ b
source
@[simp]
theorem zero_le_mul_right {α : Type u} [linear_ordered_semiring α] {b c : α} (h : 0 < c) :
0 ≤ b * c ↔ 0 ≤ b
source
@[simp]
theorem zero_lt_mul_left {α : Type u} [linear_ordered_semiring α] {b c : α} (h : 0 < c) :
0 < c * b ↔ 0 < b
source
@[simp]
theorem zero_lt_mul_right {α : Type u} [linear_ordered_semiring α] {b c : α} (h : 0 < c) :
0 < b * c ↔ 0 < b
source
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
source
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
source
theorem add_le_mul {α : Type u} [linear_ordered_semiring α] {a b : α} (a2 : 2 ≤ a) (b2 : 2 ≤ b) :
a + b ≤ a * b
source
theorem add_le_mul' {α : Type u} [linear_ordered_semiring α] {a b : α} (a2 : 2 ≤ a) (b2 : 2 ≤ b) :
a + b ≤ b * a
source
@[simp]
theorem bit0_le_bit0 {α : Type u} [linear_ordered_semiring α] {a b : α} [nontrivial α] :
bit0 a ≤ bit0 b ↔ a ≤ b
source
@[simp]
theorem bit0_lt_bit0 {α : Type u} [linear_ordered_semiring α] {a b : α} [nontrivial α] :
bit0 a < bit0 b ↔ a < b
source
@[simp]
theorem bit1_le_bit1 {α : Type u} [linear_ordered_semiring α] {a b : α} [nontrivial α] :
bit1 a ≤ bit1 b ↔ a ≤ b
source
@[simp]
theorem bit1_lt_bit1 {α : Type u} [linear_ordered_semiring α] {a b : α} [nontrivial α] :
bit1 a < bit1 b ↔ a < b
source
@[simp]
theorem one_le_bit1 {α : Type u} [linear_ordered_semiring α] {a : α} [nontrivial α] :
1 ≤ bit1 a ↔ 0 ≤ a
source
@[simp]
theorem one_lt_bit1 {α : Type u} [linear_ordered_semiring α] {a : α} [nontrivial α] :
1 < bit1 a ↔ 0 < a
source
@[simp]
theorem zero_le_bit0 {α : Type u} [linear_ordered_semiring α] {a : α} [nontrivial α] :
0 ≤ bit0 a ↔ 0 ≤ a
source
@[simp]
theorem zero_lt_bit0 {α : Type u} [linear_ordered_semiring α] {a : α} [nontrivial α] :
0 < bit0 a ↔ 0 < a
source
theorem le_mul_iff_one_le_left {α : Type u} [linear_ordered_semiring α] {a b : α} (hb : 0 < b) :
b ≤ a * b ↔ 1 ≤ a
source
theorem lt_mul_iff_one_lt_left {α : Type u} [linear_ordered_semiring α] {a b : α} (hb : 0 < b) :
b < a * b ↔ 1 < a
source
theorem le_mul_iff_one_le_right {α : Type u} [linear_ordered_semiring α] {a b : α} (hb : 0 < b) :
b ≤ b * a ↔ 1 ≤ a
source
theorem lt_mul_iff_one_lt_right {α : Type u} [linear_ordered_semiring α] {a b : α} (hb : 0 < b) :
b < b * a ↔ 1 < a
source
theorem mul_nonneg_iff_right_nonneg_of_pos {α : Type u} [linear_ordered_semiring α] {a b : α} (ha : 0 < a) :
0 ≤ b * a ↔ 0 ≤ b
source
theorem mul_le_iff_le_one_left {α : Type u} [linear_ordered_semiring α] {a b : α} (hb : 0 < b) :
a * b ≤ b ↔ a ≤ 1
source
theorem mul_lt_iff_lt_one_left {α : Type u} [linear_ordered_semiring α] {a b : α} (hb : 0 < b) :
a * b < b ↔ a < 1
source
theorem mul_le_iff_le_one_right {α : Type u} [linear_ordered_semiring α] {a b : α} (hb : 0 < b) :
b * a ≤ b ↔ a ≤ 1
source
theorem mul_lt_iff_lt_one_right {α : Type u} [linear_ordered_semiring α] {a b : α} (hb : 0 < b) :
b * a < b ↔ a < 1
source
theorem nonpos_of_mul_nonneg_left {α : Type u} [linear_ordered_semiring α] {a b : α} (h : 0 ≤ a * b) (hb : b < 0) :
a ≤ 0
source
theorem nonpos_of_mul_nonneg_right {α : Type u} [linear_ordered_semiring α] {a b : α} (h : 0 ≤ a * b) (ha : a < 0) :
b ≤ 0
source
theorem neg_of_mul_pos_left {α : Type u} [linear_ordered_semiring α] {a b : α} (h : 0 < a * b) (hb : b ≤ 0) :
a < 0
source
theorem neg_of_mul_pos_right {α : Type u} [linear_ordered_semiring α] {a b : α} (h : 0 < a * b) (ha : a ≤ 0) :
b < 0
source
@[protected, instance]
def linear_ordered_semiring.to_no_top_order {α : Type u_1} [linear_ordered_semiring α] :
no_top_order α
source
def function.injective.linear_ordered_semiring {α : Type u} [linear_ordered_semiring α] {β : 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) :
linear_ordered_semiring β

Pullback a linear_ordered_semiring under an injective map.

Equations
source
theorem monotone_mul_left_of_nonneg {α : Type u} [linear_ordered_semiring α] {a : α} (ha : 0 ≤ a) :
monotone (λ (x : α), a * x)
source
theorem monotone_mul_right_of_nonneg {α : Type u} [linear_ordered_semiring α] {a : α} (ha : 0 ≤ a) :
monotone (λ (x : α), x * a)
source
theorem monotone.mul_const {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [preorder β] {f : β → α} {a : α} (hf : monotone f) (ha : 0 ≤ a) :
monotone (λ (x : β), (f x) * a)
source
theorem monotone.const_mul {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [preorder β] {f : β → α} {a : α} (hf : monotone f) (ha : 0 ≤ a) :
monotone (λ (x : β), a * f x)
source
theorem monotone.mul {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [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)
source
theorem strict_mono_mul_left_of_pos {α : Type u} [linear_ordered_semiring α] {a : α} (ha : 0 < a) :
strict_mono (λ (x : α), a * x)
source
theorem strict_mono_mul_right_of_pos {α : Type u} [linear_ordered_semiring α] {a : α} (ha : 0 < a) :
strict_mono (λ (x : α), x * a)
source
theorem strict_mono.mul_const {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [preorder β] {f : β → α} {a : α} (hf : strict_mono f) (ha : 0 < a) :
strict_mono (λ (x : β), (f x) * a)
source
theorem strict_mono.const_mul {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [preorder β] {f : β → α} {a : α} (hf : strict_mono f) (ha : 0 < a) :
strict_mono (λ (x : β), a * f x)
source
theorem strict_mono.mul_monotone {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [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)
source
theorem monotone.mul_strict_mono {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [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)
source
theorem strict_mono.mul {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [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)
source
theorem mul_max_of_nonneg {α : Type u} [linear_ordered_semiring α] {a : α} (b c : α) (ha : 0 ≤ a) :
a * max b c = max (a * b) (a * c)
source
theorem mul_min_of_nonneg {α : Type u} [linear_ordered_semiring α] {a : α} (b c : α) (ha : 0 ≤ a) :
a * min b c = min (a * b) (a * c)
source
theorem max_mul_of_nonneg {α : Type u} [linear_ordered_semiring α] {c : α} (a b : α) (hc : 0 ≤ c) :
(max a b) * c = max (a * c) (b * c)
source
theorem min_mul_of_nonneg {α : Type u} [linear_ordered_semiring α] {c : α} (a b : α) (hc : 0 ≤ c) :
(min a b) * c = min (a * c) (b * c)
source
@[instance]
def ordered_ring.to_ordered_add_comm_group (α : Type u) [self : ordered_ring α] :
ordered_add_comm_group α
source
@[class]
structure ordered_ring (α : Type u) :
Type 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
  • nsmul : ℕ → α → α
  • nsmul_zero' : (∀ (x : α), ordered_ring.nsmul 0 x = 0) . "try_refl_tac"
  • nsmul_succ' : (∀ (n : ℕ) (x : α), ordered_ring.nsmul n.succ x = x + ordered_ring.nsmul n x) . "try_refl_tac"
  • neg : α → α
  • sub : α → α → α
  • sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
  • gsmul : ℤ → α → α
  • gsmul_zero' : (∀ (a : α), ordered_ring.gsmul 0 a = 0) . "try_refl_tac"
  • gsmul_succ' : (∀ (n : ℕ) (a : α), ordered_ring.gsmul (int.of_nat n.succ) a = a + ordered_ring.gsmul (int.of_nat n) a) . "try_refl_tac"
  • gsmul_neg' : (∀ (n : ℕ) (a : α), ordered_ring.gsmul -[1+ n] a = -ordered_ring.gsmul ↑(n.succ) 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_1 : α), (a * b) * c_1 = a * b * c_1
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • npow : ℕ → α → α
  • npow_zero' : (∀ (x : α), ordered_ring.npow 0 x = 1) . "try_refl_tac"
  • npow_succ' : (∀ (n : ℕ) (x : α), ordered_ring.npow n.succ x = x * ordered_ring.npow n x) . "try_refl_tac"
  • 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 ≤ b → b ≤ c_1 → a ≤ c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = 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 < a → 0 < b → 0 < a * b

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

Instances
source
@[instance]
def ordered_ring.to_ring (α : Type u) [self : ordered_ring α] :
ring α
source
@[protected]
theorem decidable.ordered_ring.mul_nonneg {α : Type u} [ordered_ring α] [decidable_rel has_le.le] {a b : α} (h₁ : 0 ≤ a) (h₂ : 0 ≤ b) :
0 ≤ a * b
source
theorem ordered_ring.mul_nonneg {α : Type u} [ordered_ring α] {a b : α} :
0 ≤ a → 0 ≤ b → 0 ≤ a * b
source
@[protected]
theorem decidable.ordered_ring.mul_le_mul_of_nonneg_left {α : Type u} [ordered_ring α] {a b c : α} [decidable_rel has_le.le] (h₁ : a ≤ b) (h₂ : 0 ≤ c) :
c * a ≤ c * b
source
theorem ordered_ring.mul_le_mul_of_nonneg_left {α : Type u} [ordered_ring α] {a b c : α} :
a ≤ b → 0 ≤ c → c * a ≤ c * b
source
@[protected]
theorem decidable.ordered_ring.mul_le_mul_of_nonneg_right {α : Type u} [ordered_ring α] {a b c : α} [decidable_rel has_le.le] (h₁ : a ≤ b) (h₂ : 0 ≤ c) :
a * c ≤ b * c
source
theorem ordered_ring.mul_le_mul_of_nonneg_right {α : Type u} [ordered_ring α] {a b c : α} :
a ≤ b → 0 ≤ c → a * c ≤ b * c
source
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
source
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
source
@[protected, instance]
def ordered_ring.to_ordered_semiring {α : Type u} [ordered_ring α] :
ordered_semiring α
Equations
source
@[protected]
theorem decidable.mul_le_mul_of_nonpos_left {α : Type u} [ordered_ring α] [decidable_rel has_le.le] {a b c : α} (h : b ≤ a) (hc : c ≤ 0) :
c * a ≤ c * b
source
theorem mul_le_mul_of_nonpos_left {α : Type u} [ordered_ring α] {a b c : α} :
b ≤ a → c ≤ 0 → c * a ≤ c * b
source
@[protected]
theorem decidable.mul_le_mul_of_nonpos_right {α : Type u} [ordered_ring α] [decidable_rel has_le.le] {a b c : α} (h : b ≤ a) (hc : c ≤ 0) :
a * c ≤ b * c
source
theorem mul_le_mul_of_nonpos_right {α : Type u} [ordered_ring α] {a b c : α} :
b ≤ a → c ≤ 0 → a * c ≤ b * c
source
@[protected]
theorem decidable.mul_nonneg_of_nonpos_of_nonpos {α : Type u} [ordered_ring α] [decidable_rel has_le.le] {a b : α} (ha : a ≤ 0) (hb : b ≤ 0) :
0 ≤ a * b
source
theorem mul_nonneg_of_nonpos_of_nonpos {α : Type u} [ordered_ring α] {a b : α} :
a ≤ 0 → b ≤ 0 → 0 ≤ a * b
source
theorem mul_lt_mul_of_neg_left {α : Type u} [ordered_ring α] {a b c : α} (h : b < a) (hc : c < 0) :
c * a < c * b
source
theorem mul_lt_mul_of_neg_right {α : Type u} [ordered_ring α] {a b c : α} (h : b < a) (hc : c < 0) :
a * c < b * c
source
theorem mul_pos_of_neg_of_neg {α : Type u} [ordered_ring α] {a b : α} (ha : a < 0) (hb : b < 0) :
0 < a * b
source
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) :
ordered_ring β

Pullback an ordered_ring under an injective map.

Equations
source
@[instance]
def ordered_comm_ring.to_comm_ring (α : Type u) [self : ordered_comm_ring α] :
comm_ring α
source
@[instance]
def ordered_comm_ring.to_ordered_ring (α : Type u) [self : ordered_comm_ring α] :
ordered_ring α
source
@[class]
structure ordered_comm_ring (α : Type u) :
Type 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
  • nsmul : ℕ → α → α
  • nsmul_zero' : (∀ (x : α), ordered_comm_ring.nsmul 0 x = 0) . "try_refl_tac"
  • nsmul_succ' : (∀ (n : ℕ) (x : α), ordered_comm_ring.nsmul n.succ x = x + ordered_comm_ring.nsmul n x) . "try_refl_tac"
  • neg : α → α
  • sub : α → α → α
  • sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
  • gsmul : ℤ → α → α
  • gsmul_zero' : (∀ (a : α), ordered_comm_ring.gsmul 0 a = 0) . "try_refl_tac"
  • gsmul_succ' : (∀ (n : ℕ) (a : α), ordered_comm_ring.gsmul (int.of_nat n.succ) a = a + ordered_comm_ring.gsmul (int.of_nat n) a) . "try_refl_tac"
  • gsmul_neg' : (∀ (n : ℕ) (a : α), ordered_comm_ring.gsmul -[1+ n] a = -ordered_comm_ring.gsmul ↑(n.succ) 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_1 : α), (a * b) * c_1 = a * b * c_1
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • npow : ℕ → α → α
  • npow_zero' : (∀ (x : α), ordered_comm_ring.npow 0 x = 1) . "try_refl_tac"
  • npow_succ' : (∀ (n : ℕ) (x : α), ordered_comm_ring.npow n.succ x = x * ordered_comm_ring.npow n x) . "try_refl_tac"
  • 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 ≤ b → b ≤ c_1 → a ≤ c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = 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 < a → 0 < b → 0 < a * b
  • zero_mul : ∀ (a : α), 0 * a = 0
  • mul_zero : ∀ (a : α), a * 0 = 0
  • add_left_cancel : ∀ (a b c_1 : α), a + b = a + c_1 → b = c_1
  • le_of_add_le_add_left : ∀ (a b c_1 : α), a + b ≤ a + c_1 → b ≤ c_1
  • mul_lt_mul_of_pos_left : ∀ (a b c_1 : α), a < b → 0 < c_1 → c_1 * a < c_1 * b
  • mul_lt_mul_of_pos_right : ∀ (a b c_1 : α), a < b → 0 < c_1 → a * c_1 < b * c_1
  • mul_comm : ∀ (a b : α), a * b = b * a

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

Instances
source
@[instance]
def ordered_comm_ring.to_ordered_comm_semiring (α : Type u) [self : ordered_comm_ring α] :
ordered_comm_semiring α
source
def function.injective.ordered_comm_ring {α : Type u} [ordered_comm_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) :
ordered_comm_ring β

Pullback an ordered_comm_ring under an injective map.

Equations
source
@[instance]
def linear_ordered_ring.to_nontrivial (α : Type u) [self : linear_ordered_ring α] :
nontrivial α
source
@[instance]
def linear_ordered_ring.to_linear_order (α : Type u) [self : linear_ordered_ring α] :
linear_order α
source
@[class]
structure linear_ordered_ring (α : Type u) :
Type u

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

Instances
source
@[instance]
def linear_ordered_ring.to_ordered_ring (α : Type u) [self : linear_ordered_ring α] :
ordered_ring α
source
@[protected, instance]
def linear_ordered_ring.to_linear_ordered_add_comm_group {α : Type u} [s : linear_ordered_ring α] :
linear_ordered_add_comm_group α
Equations
source
@[protected, instance]
def linear_ordered_ring.to_linear_ordered_semiring {α : Type u} [linear_ordered_ring α] :
linear_ordered_semiring α
Equations
source
@[protected, instance]
def linear_ordered_ring.to_domain {α : Type u} [linear_ordered_ring α] :
domain α
Equations
source
@[simp]
theorem abs_one {α : Type u} [linear_ordered_ring α] :
abs 1 = 1
source
@[simp]
theorem abs_two {α : Type u} [linear_ordered_ring α] :
abs 2 = 2
source
theorem abs_mul {α : Type u} [linear_ordered_ring α] (a b : α) :
abs (a * b) = (abs a) * abs b
source
def abs_hom {α : Type u} [linear_ordered_ring α] :
monoid_with_zero_hom α α

abs as a monoid_with_zero_hom.

Equations
source
@[simp]
theorem abs_mul_abs_self {α : Type u} [linear_ordered_ring α] (a : α) :
(abs a) * abs a = a * a
source
@[simp]
theorem abs_mul_self {α : Type u} [linear_ordered_ring α] (a : α) :
abs (a * a) = a * a
source
theorem mul_pos_iff {α : Type u} [linear_ordered_ring α] {a b : α} :
0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
source
theorem mul_neg_iff {α : Type u} [linear_ordered_ring α] {a b : α} :
a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
source
theorem mul_nonneg_iff {α : Type u} [linear_ordered_ring α] {a b : α} :
0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
source
theorem mul_nonpos_iff {α : Type u} [linear_ordered_ring α] {a b : α} :
a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
source
theorem mul_self_nonneg {α : Type u} [linear_ordered_ring α] (a : α) :
0 ≤ a * a
source
@[simp]
theorem neg_le_self_iff {α : Type u} [linear_ordered_ring α] {a : α} :
-a ≤ a ↔ 0 ≤ a
source
@[simp]
theorem neg_lt_self_iff {α : Type u} [linear_ordered_ring α] {a : α} :
-a < a ↔ 0 < a
source
@[simp]
theorem le_neg_self_iff {α : Type u} [linear_ordered_ring α] {a : α} :
a ≤ -a ↔ a ≤ 0
source
@[simp]
theorem lt_neg_self_iff {α : Type u} [linear_ordered_ring α] {a : α} :
a < -a ↔ a < 0
source
@[simp]
theorem abs_eq_self {α : Type u} [linear_ordered_ring α] {a : α} :
abs a = a ↔ 0 ≤ a
source
@[simp]
theorem abs_eq_neg_self {α : Type u} [linear_ordered_ring α] {a : α} :
abs a = -a ↔ a ≤ 0
source
theorem gt_of_mul_lt_mul_neg_left {α : Type u} [linear_ordered_ring α] {a b c : α} (h : c * a < c * b) (hc : c ≤ 0) :
b < a
source
theorem neg_one_lt_zero {α : Type u} [linear_ordered_ring α] :
-1 < 0
source
theorem le_of_mul_le_of_one_le {α : Type u} [linear_ordered_ring α] {a b c : α} (h : a * c ≤ b) (hb : 0 ≤ b) (hc : 1 ≤ c) :
a ≤ b
source
theorem nonneg_le_nonneg_of_sq_le_sq {α : Type u} [linear_ordered_ring α] {a b : α} (hb : 0 ≤ b) (h : a * a ≤ b * b) :
a ≤ b
source
theorem mul_self_le_mul_self_iff {α : Type u} [linear_ordered_ring α] {a b : α} (h1 : 0 ≤ a) (h2 : 0 ≤ b) :
a ≤ b ↔ a * a ≤ b * b
source
theorem mul_self_lt_mul_self_iff {α : Type u} [linear_ordered_ring α] {a b : α} (h1 : 0 ≤ a) (h2 : 0 ≤ b) :
a < b ↔ a * a < b * b
source
theorem mul_self_inj {α : Type u} [linear_ordered_ring α] {a b : α} (h1 : 0 ≤ a) (h2 : 0 ≤ b) :
a * a = b * b ↔ a = b
source
@[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
source
@[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
source
@[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
source
@[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
source
theorem sub_one_lt {α : Type u} [linear_ordered_ring α] (a : α) :
a - 1 < a
source
theorem mul_self_pos {α : Type u} [linear_ordered_ring α] {a : α} (ha : a ≠ 0) :
0 < a * a
source
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
source
theorem nonneg_of_mul_nonpos_left {α : Type u} [linear_ordered_ring α] {a b : α} (h : a * b ≤ 0) (hb : b < 0) :
0 ≤ a
source
theorem nonneg_of_mul_nonpos_right {α : Type u} [linear_ordered_ring α] {a b : α} (h : a * b ≤ 0) (ha : a < 0) :
0 ≤ b
source
theorem pos_of_mul_neg_left {α : Type u} [linear_ordered_ring α] {a b : α} (h : a * b < 0) (hb : b ≤ 0) :
0 < a
source
theorem pos_of_mul_neg_right {α : Type u} [linear_ordered_ring α] {a b : α} (h : a * b < 0) (ha : a ≤ 0) :
0 < b
source
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.

source
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
source
theorem abs_eq_iff_mul_self_eq {α : Type u} [linear_ordered_ring α] {a b : α} :
abs a = abs b ↔ a * a = b * b
source
theorem abs_lt_iff_mul_self_lt {α : Type u} [linear_ordered_ring α] {a b : α} :
abs a < abs b ↔ a * a < b * b
source
theorem abs_le_iff_mul_self_le {α : Type u} [linear_ordered_ring α] {a b : α} :
abs a ≤ abs b ↔ a * a ≤ b * b
source
theorem abs_le_one_iff_mul_self_le_one {α : Type u} [linear_ordered_ring α] {a : α} :
abs a ≤ 1 ↔ a * a ≤ 1
source
def function.injective.linear_ordered_ring {α : Type u} [linear_ordered_ring α] {β : 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) :
linear_ordered_ring β

Pullback a linear_ordered_ring under an injective map.

Equations
source
@[class]
structure linear_ordered_comm_ring (α : Type u) :
Type u

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
source
@[instance]
def linear_ordered_comm_ring.to_linear_ordered_ring (α : Type u) [self : linear_ordered_comm_ring α] :
linear_ordered_ring α
source
@[instance]
def linear_ordered_comm_ring.to_comm_monoid (α : Type u) [self : linear_ordered_comm_ring α] :
comm_monoid α
source
@[protected, instance]
def linear_ordered_comm_ring.to_ordered_comm_ring {α : Type u} [d : linear_ordered_comm_ring α] :
ordered_comm_ring α
Equations
source
@[protected, instance]
def linear_ordered_comm_ring.to_integral_domain {α : Type u} [s : linear_ordered_comm_ring α] :
integral_domain α
Equations
source
@[protected, instance]
def linear_ordered_comm_ring.to_linear_ordered_semiring {α : Type u} [d : linear_ordered_comm_ring α] :
linear_ordered_semiring α
Equations
source
theorem max_mul_mul_le_max_mul_max {α : Type u} [linear_ordered_comm_ring α] {a d : α} (b c : α) (ha : 0 ≤ a) (hd : 0 ≤ d) :
max (a * b) (d * c) ≤ (max a c) * max d b
source
theorem abs_sub_sq {α : Type u} [linear_ordered_comm_ring α] (a b : α) :
(abs (a - b)) * abs (a - b) = a * a + b * b - ((1 + 1) * a) * b
source
def function.injective.linear_ordered_comm_ring {α : Type u} [linear_ordered_comm_ring α] {β : 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) :
linear_ordered_comm_ring β

Pullback a linear_ordered_comm_ring under an injective map.

Equations
source
@[instance]
def nonneg_ring.to_ring (α : Type u_1) [self : nonneg_ring α] :
ring α
source
@[class]
structure nonneg_ring (α : Type u_1) :
Type u_1

Extend nonneg_add_comm_group to support ordered rings specified by their nonnegative elements

Instances
source
@[instance]
def nonneg_ring.to_nonneg_add_comm_group (α : Type u_1) [self : nonneg_ring α] :
nonneg_add_comm_group α
source
@[class]
structure linear_nonneg_ring (α : Type u_1) :
Type u_1

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

source
@[instance]
def linear_nonneg_ring.to_domain (α : Type u_1) [self : linear_nonneg_ring α] :
domain α
source
@[instance]
def linear_nonneg_ring.to_nonneg_add_comm_group (α : Type u_1) [self : linear_nonneg_ring α] :
nonneg_add_comm_group α
source
def nonneg_ring.to_linear_nonneg_ring {α : Type u} [nonneg_ring α] [nontrivial α] [decidable_pred nonneg_ring.nonneg] (nonneg_total : ∀ (a : α), nonneg_ring.nonneg a ∨ nonneg_ring.nonneg (-a)) :
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
source
@[protected, instance]
def linear_nonneg_ring.to_nonneg_ring {α : Type u} [linear_nonneg_ring α] :
nonneg_ring α
Equations
source
def linear_nonneg_ring.to_linear_order {α : Type u} [linear_nonneg_ring α] [decidable_pred linear_nonneg_ring.nonneg] :
linear_order α

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

Equations
source
def linear_nonneg_ring.to_linear_ordered_ring {α : Type u} [linear_nonneg_ring α] [decidable_pred linear_nonneg_ring.nonneg] :
linear_ordered_ring α

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

Equations
source
def linear_nonneg_ring.to_linear_ordered_comm_ring {α : Type u} [linear_nonneg_ring α] [decidable_pred linear_nonneg_ring.nonneg] [comm : is_commutative α has_mul.mul] :
linear_ordered_comm_ring α

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

Equations
source
@[class]
structure canonically_ordered_comm_semiring (α : Type u_1) :
Type u_1

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
source
@[instance]
def canonically_ordered_comm_semiring.to_comm_semiring (α : Type u_1) [self : canonically_ordered_comm_semiring α] :
comm_semiring α
source
@[instance]
def canonically_ordered_comm_semiring.to_canonically_ordered_add_monoid (α : Type u_1) [self : canonically_ordered_comm_semiring α] :
canonically_ordered_add_monoid α
source
@[protected, instance]
def canonically_ordered_semiring.canonically_ordered_comm_semiring.to_no_zero_divisors {α : Type u} [canonically_ordered_comm_semiring α] :
no_zero_divisors α
source
theorem canonically_ordered_semiring.mul_le_mul {α : Type u} [canonically_ordered_comm_semiring α] {a b c d : α} (hab : a ≤ b) (hcd : c ≤ d) :
a * c ≤ b * d
source
theorem canonically_ordered_semiring.mul_le_mul_left' {α : Type u} [canonically_ordered_comm_semiring α] {b c : α} (h : b ≤ c) (a : α) :
a * b ≤ a * c
source
theorem canonically_ordered_semiring.mul_le_mul_right' {α : Type u} [canonically_ordered_comm_semiring α] {b c : α} (h : b ≤ c) (a : α) :
b * a ≤ c * a
source
theorem canonically_ordered_semiring.zero_lt_one {α : Type u} [canonically_ordered_comm_semiring α] [nontrivial α] :
0 < 1

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

source
theorem canonically_ordered_semiring.mul_pos {α : Type u} [canonically_ordered_comm_semiring α] {a b : α} :
0 < a * b ↔ 0 < a ∧ 0 < b
source
@[protected, instance]
def with_top.nontrivial {α : Type u} [nonempty α] :
nontrivial (with_top α)
source
@[protected, instance]
def with_top.mul_zero_class {α : Type u} [decidable_eq α] [has_zero α] [has_mul α] :
mul_zero_class (with_top α)
Equations
source
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)))
source
@[simp]
theorem with_top.mul_top {α : Type u} [decidable_eq α] [has_zero α] [has_mul α] {a : with_top α} (h : a ≠ 0) :
a * ⊤ = ⊤
source
@[simp]
theorem with_top.top_mul {α : Type u} [decidable_eq α] [has_zero α] [has_mul α] {a : with_top α} (h : a ≠ 0) :
⊤ * a = ⊤
source
@[simp]
theorem with_top.top_mul_top {α : Type u} [decidable_eq α] [has_zero α] [has_mul α] :
⊤ * ⊤ = ⊤
source
@[norm_cast]
theorem with_top.coe_mul {α : Type u} [decidable_eq α] [mul_zero_class α] {a b : α} :
↑a * b = (↑a) * ↑b
source
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)
source
@[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
source
@[protected, instance]
def with_top.no_zero_divisors {α : Type u} [decidable_eq α] [mul_zero_class α] [no_zero_divisors α] :
no_zero_divisors (with_top α)
source
@[protected, instance]
def with_top.canonically_ordered_comm_semiring {α : Type u} [decidable_eq α] [canonically_ordered_comm_semiring α] [nontrivial α] :
canonically_ordered_comm_semiring (with_top α)
Equations
source
theorem with_top.mul_lt_top {α : Type u} [decidable_eq α] [canonically_ordered_comm_semiring α] [nontrivial α] {a b : with_top α} (ha : a < ⊤) (hb : b < ⊤) :
a * b < ⊤