mathlib docs: algebra.ordered

source

@[instance]

def ordered_semiring.to_semiring (α : Type u) [s : 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
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_1 → b = c_1
add_right_cancel : ∀ (a b c_1 : α), a + b = c_1 + b → a = 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
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) [s : ordered_semiring α] :

ordered_cancel_add_comm_monoid α

source

theorem mul_lt_mul_of_pos_left {α : Type u} [ordered_semiring α] {a b c : α} :

a < b → 0 < c → c * a < c * b

source

theorem mul_lt_mul_of_pos_right {α : Type u} [ordered_semiring α] {a b c : α} :

a < b → 0 < c → a * c < b * c

source

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

a ≤ b → 0 ≤ c → c * a ≤ c * b

source

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

a ≤ b → 0 ≤ c → a * c ≤ b * c

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

theorem mul_nonneg {α : Type u} [ordered_semiring α] {a b : α} :

0 ≤ a → 0 ≤ b → 0 ≤ a * b

source

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

0 ≤ a → b ≤ 0 → 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

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_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 : α} :

0 < a → 0 < b → 0 < a * b

source

theorem mul_neg_of_pos_of_neg {α : Type u} [ordered_semiring α] {a b : α} :

0 < a → b < 0 → a * b < 0

source

theorem mul_neg_of_neg_of_pos {α : Type u} [ordered_semiring α] {a b : α} :

a < 0 → 0 < b → a * b < 0

source

theorem mul_self_le_mul_self {α : Type u} [ordered_semiring α] {a b : α} :

0 ≤ a → a ≤ b → a * a ≤ b * b

source

theorem mul_self_lt_mul_self {α : Type u} [ordered_semiring α] {a b : α} :

0 ≤ a → a < b → a * a < b * b

source

@[instance]

def linear_ordered_semiring.to_ordered_semiring (α : Type u) [s : 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
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_1 → b = c_1
add_right_cancel : ∀ (a b c_1 : α), a + b = c_1 + b → a = 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
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
zero_lt_one : linear_ordered_semiring.zero < linear_ordered_semiring.one

A linear_ordered_semiring α is a 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) [s : linear_ordered_semiring α] :

linear_order α

source

theorem zero_lt_one {α : Type u} [linear_ordered_semiring α] :

0 < 1

source

theorem zero_le_one {α : Type u} [linear_ordered_semiring α] :

0 ≤ 1

source

theorem two_pos {α : Type u} [linear_ordered_semiring α] :

0 < 2

source

theorem two_ne_zero {α : Type u} [linear_ordered_semiring α] :

2 ≠ 0

source

theorem one_lt_two {α : Type u} [linear_ordered_semiring α] :

1 < 2

source

theorem one_le_two {α : Type u} [linear_ordered_semiring α] :

1 ≤ 2

source

theorem four_pos {α : Type u} [linear_ordered_semiring α] :

0 < 4

source

theorem lt_of_mul_lt_mul_left {α : Type u} [linear_ordered_semiring α] {a b c : α} :

c * a < c * b → 0 ≤ c → a < b

source

theorem lt_of_mul_lt_mul_right {α : Type u} [linear_ordered_semiring α] {a b c : α} :

a * c < b * c → 0 ≤ c → a < b

source

theorem le_of_mul_le_mul_left {α : Type u} [linear_ordered_semiring α] {a b c : α} :

c * a ≤ c * b → 0 < c → a ≤ b

source

theorem le_of_mul_le_mul_right {α : Type u} [linear_ordered_semiring α] {a b c : α} :

a * c ≤ b * c → 0 < c → a ≤ b

source

theorem pos_of_mul_pos_left {α : Type u} [linear_ordered_semiring α] {a b : α} :

0 < a * b → 0 ≤ a → 0 < b

source

theorem pos_of_mul_pos_right {α : Type u} [linear_ordered_semiring α] {a b : α} :

0 < a * b → 0 ≤ b → 0 < a

source

theorem nonneg_of_mul_nonneg_left {α : Type u} [linear_ordered_semiring α] {a b : α} :

0 ≤ a * b → 0 < a → 0 ≤ b

source

theorem nonneg_of_mul_nonneg_right {α : Type u} [linear_ordered_semiring α] {a b : α} :

0 ≤ a * b → 0 < b → 0 ≤ a

source

theorem neg_of_mul_neg_left {α : Type u} [linear_ordered_semiring α] {a b : α} :

a * b < 0 → 0 ≤ a → b < 0

source

theorem neg_of_mul_neg_right {α : Type u} [linear_ordered_semiring α] {a b : α} :

a * b < 0 → 0 ≤ b → a < 0

source

theorem nonpos_of_mul_nonpos_left {α : Type u} [linear_ordered_semiring α] {a b : α} :

a * b ≤ 0 → 0 < a → b ≤ 0

source

theorem nonpos_of_mul_nonpos_right {α : Type u} [linear_ordered_semiring α] {a b : α} :

a * b ≤ 0 → 0 < b → a ≤ 0

source

theorem zero_lt_two {α : Type u} [linear_ordered_semiring α] :

0 < 2

0 < 2: an alternative version of two_pos that only assumes linear_ordered_semiring.

source

@[simp]

theorem mul_le_mul_left {α : Type u} [linear_ordered_semiring α] {a b c : α} :

0 < c → (c * a ≤ c * b ↔ a ≤ b)

source

@[simp]

theorem mul_le_mul_right {α : Type u} [linear_ordered_semiring α] {a b c : α} :

0 < c → (a * c ≤ b * c ↔ a ≤ b)

source

@[simp]

theorem mul_lt_mul_left {α : Type u} [linear_ordered_semiring α] {a b c : α} :

0 < c → (c * a < c * b ↔ a < b)

source

@[simp]

theorem mul_lt_mul_right {α : Type u} [linear_ordered_semiring α] {a b c : α} :

0 < c → (a * c < b * c ↔ a < b)

source

@[simp]

theorem zero_le_mul_left {α : Type u} [linear_ordered_semiring α] {b c : α} :

0 < c → (0 ≤ c * b ↔ 0 ≤ b)

source

@[simp]

theorem zero_le_mul_right {α : Type u} [linear_ordered_semiring α] {b c : α} :

0 < c → (0 ≤ b * c ↔ 0 ≤ b)

source

@[simp]

theorem zero_lt_mul_left {α : Type u} [linear_ordered_semiring α] {b c : α} :

0 < c → (0 < c * b ↔ 0 < b)

source

@[simp]

theorem zero_lt_mul_right {α : Type u} [linear_ordered_semiring α] {b c : α} :

0 < c → (0 < b * c ↔ 0 < b)

source

@[simp]

theorem bit0_le_bit0 {α : Type u} [linear_ordered_semiring α] {a b : α} :

bit0 a ≤ bit0 b ↔ a ≤ b

source

@[simp]

theorem bit0_lt_bit0 {α : Type u} [linear_ordered_semiring α] {a b : α} :

bit0 a < bit0 b ↔ a < b

source

@[simp]

theorem bit1_le_bit1 {α : Type u} [linear_ordered_semiring α] {a b : α} :

bit1 a ≤ bit1 b ↔ a ≤ b

source

@[simp]

theorem bit1_lt_bit1 {α : Type u} [linear_ordered_semiring α] {a b : α} :

bit1 a < bit1 b ↔ a < b

source

@[simp]

theorem one_le_bit1 {α : Type u} [linear_ordered_semiring α] {a : α} :

1 ≤ bit1 a ↔ 0 ≤ a

source

@[simp]

theorem one_lt_bit1 {α : Type u} [linear_ordered_semiring α] {a : α} :

1 < bit1 a ↔ 0 < a

source

@[simp]

theorem zero_le_bit0 {α : Type u} [linear_ordered_semiring α] {a : α} :

0 ≤ bit0 a ↔ 0 ≤ a

source

@[simp]

theorem zero_lt_bit0 {α : Type u} [linear_ordered_semiring α] {a : α} :

0 < bit0 a ↔ 0 < a

source

theorem mul_lt_mul'' {α : Type u} [linear_ordered_semiring α] {a b c d : α} :

a < c → b < d → 0 ≤ a → 0 ≤ b → a * b < c * d

source

theorem le_mul_iff_one_le_left {α : Type u} [linear_ordered_semiring α] {a b : α} :

0 < b → (b ≤ a * b ↔ 1 ≤ a)

source

theorem lt_mul_iff_one_lt_left {α : Type u} [linear_ordered_semiring α] {a b : α} :

0 < b → (b < a * b ↔ 1 < a)

source

theorem le_mul_iff_one_le_right {α : Type u} [linear_ordered_semiring α] {a b : α} :

0 < b → (b ≤ b * a ↔ 1 ≤ a)

source

theorem lt_mul_iff_one_lt_right {α : Type u} [linear_ordered_semiring α] {a b : α} :

0 < b → (b < b * a ↔ 1 < a)

source

theorem lt_mul_of_one_lt_right {α : Type u} [linear_ordered_semiring α] {a b : α} :

0 < b → 1 < a → b < b * a

source

theorem le_mul_of_one_le_right {α : Type u} [linear_ordered_semiring α] {a b : α} :

0 ≤ b → 1 ≤ a → b ≤ b * a

source

theorem le_mul_of_one_le_left {α : Type u} [linear_ordered_semiring α] {a b : α} :

0 ≤ b → 1 ≤ a → b ≤ a * b

source

theorem mul_nonneg_iff_right_nonneg_of_pos {α : Type u} [linear_ordered_semiring α] {a b : α} :

0 < a → (0 ≤ b * a ↔ 0 ≤ b)

source

theorem bit1_pos {α : Type u} [linear_ordered_semiring α] {a : α} :

0 ≤ a → 0 < bit1 a

source

theorem bit1_pos' {α : Type u} [linear_ordered_semiring α] {a : α} :

0 < a → 0 < bit1 a

source

theorem lt_add_one {α : Type u} [linear_ordered_semiring α] (a : α) :

a < a + 1

source

theorem lt_one_add {α : Type u} [linear_ordered_semiring α] (a : α) :

a < 1 + a

source

theorem one_lt_mul {α : Type u} [linear_ordered_semiring α] {a b : α} :

1 ≤ a → 1 < b → 1 < a * b

source

theorem mul_le_one {α : Type u} [linear_ordered_semiring α] {a b : α} :

a ≤ 1 → 0 ≤ b → b ≤ 1 → a * b ≤ 1

source

theorem one_lt_mul_of_le_of_lt {α : Type u} [linear_ordered_semiring α] {a b : α} :

1 ≤ a → 1 < b → 1 < a * b

source

theorem one_lt_mul_of_lt_of_le {α : Type u} [linear_ordered_semiring α] {a b : α} :

1 < a → 1 ≤ b → 1 < a * b

source

theorem mul_le_of_le_one_right {α : Type u} [linear_ordered_semiring α] {a b : α} :

0 ≤ a → b ≤ 1 → a * b ≤ a

source

theorem mul_le_of_le_one_left {α : Type u} [linear_ordered_semiring α] {a b : α} :

0 ≤ b → a ≤ 1 → a * b ≤ b

source

theorem mul_lt_one_of_nonneg_of_lt_one_left {α : Type u} [linear_ordered_semiring α] {a b : α} :

0 ≤ a → a < 1 → b ≤ 1 → a * b < 1

source

theorem mul_lt_one_of_nonneg_of_lt_one_right {α : Type u} [linear_ordered_semiring α] {a b : α} :

a ≤ 1 → 0 ≤ b → b < 1 → a * b < 1

source

theorem mul_le_iff_le_one_left {α : Type u} [linear_ordered_semiring α] {a b : α} :

0 < b → (a * b ≤ b ↔ a ≤ 1)

source

theorem mul_lt_iff_lt_one_left {α : Type u} [linear_ordered_semiring α] {a b : α} :

0 < b → (a * b < b ↔ a < 1)

source

theorem mul_le_iff_le_one_right {α : Type u} [linear_ordered_semiring α] {a b : α} :

0 < b → (b * a ≤ b ↔ a ≤ 1)

source

theorem mul_lt_iff_lt_one_right {α : Type u} [linear_ordered_semiring α] {a b : α} :

0 < b → (b * a < b ↔ a < 1)

source

theorem nonpos_of_mul_nonneg_left {α : Type u} [linear_ordered_semiring α] {a b : α} :

0 ≤ a * b → b < 0 → a ≤ 0

source

theorem nonpos_of_mul_nonneg_right {α : Type u} [linear_ordered_semiring α] {a b : α} :

0 ≤ a * b → a < 0 → b ≤ 0

source

theorem neg_of_mul_pos_left {α : Type u} [linear_ordered_semiring α] {a b : α} :

0 < a * b → b ≤ 0 → a < 0

source

theorem neg_of_mul_pos_right {α : Type u} [linear_ordered_semiring α] {a b : α} :

0 < a * b → a ≤ 0 → b < 0

source

@[instance]

def linear_ordered_semiring.to_nontrivial {α : Type u_1} [linear_ordered_semiring α] :

nontrivial α

Equations

linear_ordered_semiring.to_nontrivial = _

source

@[instance]

def linear_ordered_semiring.to_no_top_order {α : Type u_1} [linear_ordered_semiring α] :

no_top_order α

Equations

linear_ordered_semiring.to_no_top_order = _

source

theorem monotone_mul_left_of_nonneg {α : Type u} [linear_ordered_semiring α] {a : α} :

0 ≤ a → monotone (λ (x : α), a * x)

source

theorem monotone_mul_right_of_nonneg {α : Type u} [linear_ordered_semiring α] {a : α} :

0 ≤ a → monotone (λ (x : α), x * a)

source

theorem monotone.mul_const {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [preorder β] {f : β → α} {a : α} :

monotone f → 0 ≤ a → monotone (λ (x : β), f x * a)

source

theorem monotone.const_mul {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [preorder β] {f : β → α} {a : α} :

monotone f → 0 ≤ a → monotone (λ (x : β), a * f x)

source

theorem monotone.mul {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [preorder β] {f g : β → α} :

monotone f → monotone g → (∀ (x : β), 0 ≤ f x) → (∀ (x : β), 0 ≤ g x) → monotone (λ (x : β), f x * g x)

source

theorem strict_mono_mul_left_of_pos {α : Type u} [linear_ordered_semiring α] {a : α} :

0 < a → strict_mono (λ (x : α), a * x)

source

theorem strict_mono_mul_right_of_pos {α : Type u} [linear_ordered_semiring α] {a : α} :

0 < a → strict_mono (λ (x : α), x * a)

source

theorem strict_mono.mul_const {α : Type u} {β : Type u_1} [linear_ordered_semiring α] [preorder β] {f : β → α} {a : α} :

strict_mono f → 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 : α} :

strict_mono f → 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 : β → α} :

strict_mono f → monotone g → (∀ (x : β), 0 ≤ f x) → (∀ (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 : β → α} :

monotone f → strict_mono g → (∀ (x : β), 0 < f x) → (∀ (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 : β → α} :

strict_mono f → strict_mono g → (∀ (x : β), 0 ≤ f x) → (∀ (x : β), 0 ≤ g x) → strict_mono (λ (x : β), f x * g x)

source

@[instance]

def decidable_linear_ordered_semiring.to_linear_ordered_semiring (α : Type u) [s : decidable_linear_ordered_semiring α] :

linear_ordered_semiring α

source

@[instance]

def decidable_linear_ordered_semiring.to_decidable_linear_order (α : Type u) [s : decidable_linear_ordered_semiring α] :

decidable_linear_order α

source

@[class]

structure decidable_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
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_1 → b = c_1
add_right_cancel : ∀ (a b c_1 : α), a + b = c_1 + b → a = 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
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
zero_lt_one : decidable_linear_ordered_semiring.zero < decidable_linear_ordered_semiring.one
decidable_le : decidable_rel has_le.le
decidable_eq : decidable_eq α
decidable_lt : decidable_rel has_lt.lt

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

Instances

source

@[simp]

theorem decidable.mul_le_mul_left {α : Type u} [decidable_linear_ordered_semiring α] {a b c : α} :

0 < c → (c * a ≤ c * b ↔ a ≤ b)

source

@[simp]

theorem decidable.mul_le_mul_right {α : Type u} [decidable_linear_ordered_semiring α] {a b c : α} :

0 < c → (a * c ≤ b * c ↔ a ≤ b)

source

@[instance]

def ordered_ring.to_nontrivial (α : Type u) [s : ordered_ring α] :

nontrivial α

source

@[instance]

def ordered_ring.to_ring (α : Type u) [s : ordered_ring α] :

ring α

source

@[instance]

def ordered_ring.to_ordered_add_comm_group (α : Type u) [s : 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
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 ≤ 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
exists_pair_ne : ∃ (x y : α), x ≠ y
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

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

0 ≤ a → 0 ≤ b → 0 ≤ a * 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

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 : α} :

a < b → 0 < c → c * a < c * b

source

theorem ordered_ring.mul_lt_mul_of_pos_right {α : Type u} [ordered_ring α] {a b c : α} :

a < b → 0 < c → a * c < b * c

source

@[instance]

def ordered_ring.to_ordered_semiring {α : Type u} [ordered_ring α] :

ordered_semiring α

Equations

ordered_ring.to_ordered_semiring = {add := ordered_ring.add _inst_1, add_assoc := _, zero := ordered_ring.zero _inst_1, zero_add := _, add_zero := _, add_comm := _, mul := ordered_ring.mul _inst_1, mul_assoc := _, one := ordered_ring.one _inst_1, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, add_left_cancel := _, add_right_cancel := _, le := ordered_ring.le _inst_1, lt := ordered_ring.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _, mul_lt_mul_of_pos_left := _, mul_lt_mul_of_pos_right := _}

source

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

b ≤ a → c ≤ 0 → c * a ≤ c * b

source

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

b ≤ a → c ≤ 0 → a * c ≤ b * c

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 : α} :

b < a → c < 0 → c * a < c * b

source

theorem mul_lt_mul_of_neg_right {α : Type u} [ordered_ring α] {a b c : α} :

b < a → c < 0 → a * c < b * c

source

theorem mul_pos_of_neg_of_neg {α : Type u} [ordered_ring α] {a b : α} :

a < 0 → b < 0 → 0 < a * b

source

@[class]

structure linear_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
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 ≤ 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
exists_pair_ne : ∃ (x y : α), x ≠ y
mul_pos : ∀ (a b : α), 0 < a → 0 < b → 0 < a * b
le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
zero_lt_one : linear_ordered_ring.zero < linear_ordered_ring.one

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_linear_order (α : Type u) [s : linear_ordered_ring α] :

linear_order α

source

@[instance]

def linear_ordered_ring.to_ordered_ring (α : Type u) [s : linear_ordered_ring α] :

ordered_ring α

source

@[instance]

def linear_ordered_ring.to_linear_ordered_semiring {α : Type u} [linear_ordered_ring α] :

linear_ordered_semiring α

Equations

linear_ordered_ring.to_linear_ordered_semiring = {add := linear_ordered_ring.add _inst_1, add_assoc := _, zero := linear_ordered_ring.zero _inst_1, zero_add := _, add_zero := _, add_comm := _, mul := linear_ordered_ring.mul _inst_1, mul_assoc := _, one := linear_ordered_ring.one _inst_1, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, add_left_cancel := _, add_right_cancel := _, le := linear_ordered_ring.le _inst_1, lt := linear_ordered_ring.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _, mul_lt_mul_of_pos_left := _, mul_lt_mul_of_pos_right := _, le_total := _, zero_lt_one := _}

source

theorem mul_self_nonneg {α : Type u} [linear_ordered_ring α] (a : α) :

0 ≤ a * a

source

theorem pos_and_pos_or_neg_and_neg_of_mul_pos {α : Type u} [linear_ordered_ring α] {a b : α} :

0 < a * b → 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

source

theorem gt_of_mul_lt_mul_neg_left {α : Type u} [linear_ordered_ring α] {a b c : α} :

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

a * c ≤ b → 0 ≤ b → 1 ≤ c → a ≤ b

source

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

0 ≤ b → a * a ≤ b * b → a ≤ b

source

theorem mul_self_le_mul_self_iff {α : Type u} [linear_ordered_ring α] {a b : α} :

0 ≤ a → 0 ≤ b → (a ≤ b ↔ a * a ≤ b * b)

source

theorem mul_self_lt_mul_self_iff {α : Type u} [linear_ordered_ring α] {a b : α} :

0 ≤ a → 0 ≤ b → (a < b ↔ a * a < b * b)

source

theorem linear_ordered_ring.eq_zero_or_eq_zero_of_mul_eq_zero {α : Type u} [linear_ordered_ring α] {a b : α} :

a * b = 0 → a = 0 ∨ b = 0

source

@[instance]

def linear_ordered_ring.to_no_bot_order {α : Type u} [linear_ordered_ring α] :

no_bot_order α

Equations

linear_ordered_ring.to_no_bot_order = _

source

@[instance]

def linear_ordered_ring.to_domain {α : Type u} [linear_ordered_ring α] :

domain α

Equations

linear_ordered_ring.to_domain = {add := linear_ordered_ring.add _inst_1, add_assoc := _, zero := linear_ordered_ring.zero _inst_1, zero_add := _, add_zero := _, neg := linear_ordered_ring.neg _inst_1, add_left_neg := _, add_comm := _, mul := linear_ordered_ring.mul _inst_1, mul_assoc := _, one := linear_ordered_ring.one _inst_1, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}

source

@[simp]

theorem mul_le_mul_left_of_neg {α : Type u} [linear_ordered_ring α] {a b c : α} :

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 : α} :

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 : α} :

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 : α} :

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 : α} :

a ≠ 0 → 0 < a * a

source

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

x ≤ y → -x ≤ y → x * x ≤ y * y

source

theorem nonneg_of_mul_nonpos_left {α : Type u} [linear_ordered_ring α] {a b : α} :

a * b ≤ 0 → b < 0 → 0 ≤ a

source

theorem nonneg_of_mul_nonpos_right {α : Type u} [linear_ordered_ring α] {a b : α} :

a * b ≤ 0 → a < 0 → 0 ≤ b

source

theorem pos_of_mul_neg_left {α : Type u} [linear_ordered_ring α] {a b : α} :

a * b < 0 → b ≤ 0 → 0 < a

source

theorem pos_of_mul_neg_right {α : Type u} [linear_ordered_ring α] {a b : α} :

a * b < 0 → 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

source

@[class]

structure linear_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
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 ≤ 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
exists_pair_ne : ∃ (x y : α), x ≠ y
mul_pos : ∀ (a b : α), 0 < a → 0 < b → 0 < a * b
le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
zero_lt_one : linear_ordered_comm_ring.zero < linear_ordered_comm_ring.one
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

source

@[instance]

def linear_ordered_comm_ring.to_linear_ordered_ring (α : Type u) [s : linear_ordered_comm_ring α] :

linear_ordered_ring α

source

@[instance]

def linear_ordered_comm_ring.to_comm_monoid (α : Type u) [s : linear_ordered_comm_ring α] :

comm_monoid α

source

@[instance]

def linear_ordered_comm_ring.to_integral_domain {α : Type u} [s : linear_ordered_comm_ring α] :

integral_domain α

Equations

linear_ordered_comm_ring.to_integral_domain = {add := linear_ordered_comm_ring.add s, add_assoc := _, zero := linear_ordered_comm_ring.zero s, zero_add := _, add_zero := _, neg := linear_ordered_comm_ring.neg s, add_left_neg := _, add_comm := _, mul := linear_ordered_comm_ring.mul s, mul_assoc := _, one := linear_ordered_comm_ring.one s, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}

source

@[instance]

def decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_add_comm_group (α : Type u) [s : decidable_linear_ordered_comm_ring α] :

decidable_linear_ordered_add_comm_group α

source

@[class]

structure decidable_linear_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
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 ≤ 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
exists_pair_ne : ∃ (x y : α), x ≠ y
mul_pos : ∀ (a b : α), 0 < a → 0 < b → 0 < a * b
le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
zero_lt_one : decidable_linear_ordered_comm_ring.zero < decidable_linear_ordered_comm_ring.one
mul_comm : ∀ (a b : α), a * b = b * a
decidable_le : decidable_rel has_le.le
decidable_eq : decidable_eq α
decidable_lt : decidable_rel has_lt.lt

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

Instances

source

@[instance]

def decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring (α : Type u) [s : decidable_linear_ordered_comm_ring α] :

linear_ordered_comm_ring α

source

@[instance]

def decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_semiring {α : Type u} [d : decidable_linear_ordered_comm_ring α] :

decidable_linear_ordered_semiring α

Equations

decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_semiring = let s : linear_ordered_semiring α := linear_ordered_ring.to_linear_ordered_semiring in {add := decidable_linear_ordered_comm_ring.add d, add_assoc := _, zero := decidable_linear_ordered_comm_ring.zero d, zero_add := _, add_zero := _, add_comm := _, mul := decidable_linear_ordered_comm_ring.mul d, mul_assoc := _, one := decidable_linear_ordered_comm_ring.one d, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, add_left_cancel := _, add_right_cancel := _, le := decidable_linear_ordered_comm_ring.le d, lt := decidable_linear_ordered_comm_ring.lt d, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _, mul_lt_mul_of_pos_left := _, mul_lt_mul_of_pos_right := _, le_total := _, zero_lt_one := _, decidable_le := decidable_linear_ordered_comm_ring.decidable_le d, decidable_eq := decidable_linear_ordered_comm_ring.decidable_eq d, decidable_lt := decidable_linear_ordered_comm_ring.decidable_lt d}

source

theorem abs_mul {α : Type u} [decidable_linear_ordered_comm_ring α] (a b : α) :

abs (a * b) = abs a * abs b

source

theorem abs_mul_abs_self {α : Type u} [decidable_linear_ordered_comm_ring α] (a : α) :

abs a * abs a = a * a

source

theorem abs_mul_self {α : Type u} [decidable_linear_ordered_comm_ring α] (a : α) :

abs (a * a) = a * a

source

theorem sub_le_of_abs_sub_le_left {α : Type u} [decidable_linear_ordered_comm_ring α] {a b c : α} :

abs (a - b) ≤ c → b - c ≤ a

source

theorem sub_le_of_abs_sub_le_right {α : Type u} [decidable_linear_ordered_comm_ring α] {a b c : α} :

abs (a - b) ≤ c → a - c ≤ b

source

theorem sub_lt_of_abs_sub_lt_left {α : Type u} [decidable_linear_ordered_comm_ring α] {a b c : α} :

abs (a - b) < c → b - c < a

source

theorem sub_lt_of_abs_sub_lt_right {α : Type u} [decidable_linear_ordered_comm_ring α] {a b c : α} :

abs (a - b) < c → a - c < b

source

theorem abs_sub_square {α : Type u} [decidable_linear_ordered_comm_ring α] (a b : α) :

abs (a - b) * abs (a - b) = a * a + b * b - (1 + 1) * a * b

source

theorem eq_zero_of_mul_self_add_mul_self_eq_zero {α : Type u} [decidable_linear_ordered_comm_ring α] {a b : α} :

a * a + b * b = 0 → a = 0

source

theorem abs_abs_sub_abs_le_abs_sub {α : Type u} [decidable_linear_ordered_comm_ring α] (a b : α) :

abs (abs a - abs b) ≤ abs (a - b)

source

@[simp]

theorem abs_two {α : Type u} [decidable_linear_ordered_comm_ring α] :

abs 2 = 2

source

@[instance]

def nonneg_ring.to_nontrivial (α : Type u_1) [s : nonneg_ring α] :

nontrivial α

source

@[instance]

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

ring α

source

@[class]

structure nonneg_ring :

Type u_1 → Type 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
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
nonneg : α → Prop
pos : α → Prop
pos_iff : (∀ (a : α), nonneg_ring.pos a ↔ nonneg_ring.nonneg a ∧ ¬nonneg_ring.nonneg (-a)) . "order_laws_tac"
zero_nonneg : nonneg_ring.nonneg 0
add_nonneg : ∀ {a b : α}, nonneg_ring.nonneg a → nonneg_ring.nonneg b → nonneg_ring.nonneg (a + b)
nonneg_antisymm : ∀ {a : α}, nonneg_ring.nonneg a → nonneg_ring.nonneg (-a) → a = 0
exists_pair_ne : ∃ (x y : α), x ≠ y
mul_nonneg : ∀ {a b : α}, nonneg_ring.nonneg a → nonneg_ring.nonneg b → nonneg_ring.nonneg (a * b)
mul_pos : ∀ {a b : α}, nonneg_ring.pos a → nonneg_ring.pos b → nonneg_ring.pos (a * b)

Extend nonneg_add_comm_group to support ordered rings specified by their nonnegative elements

Instances

linear_nonneg_ring.to_nonneg_ring

source

@[instance]

def nonneg_ring.to_nonneg_add_comm_group (α : Type u_1) [s : nonneg_ring α] :

nonneg_add_comm_group α

source

@[instance]

def linear_nonneg_ring.to_nonneg_add_comm_group (α : Type u_1) [s : linear_nonneg_ring α] :

nonneg_add_comm_group α

source

@[instance]

def linear_nonneg_ring.to_domain (α : Type u_1) [s : linear_nonneg_ring α] :

domain α

source

@[class]

structure linear_nonneg_ring :

Type u_1 → Type 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
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
exists_pair_ne : ∃ (x y : α), x ≠ y
eq_zero_or_eq_zero_of_mul_eq_zero : ∀ (a b : α), a * b = 0 → a = 0 ∨ b = 0
nonneg : α → Prop
pos : α → Prop
pos_iff : (∀ (a : α), linear_nonneg_ring.pos a ↔ linear_nonneg_ring.nonneg a ∧ ¬linear_nonneg_ring.nonneg (-a)) . "order_laws_tac"
zero_nonneg : linear_nonneg_ring.nonneg 0
add_nonneg : ∀ {a b : α}, linear_nonneg_ring.nonneg a → linear_nonneg_ring.nonneg b → linear_nonneg_ring.nonneg (a + b)
nonneg_antisymm : ∀ {a : α}, linear_nonneg_ring.nonneg a → linear_nonneg_ring.nonneg (-a) → a = 0
mul_nonneg : ∀ {a b : α}, linear_nonneg_ring.nonneg a → linear_nonneg_ring.nonneg b → linear_nonneg_ring.nonneg (a * b)
nonneg_total : ∀ (a : α), linear_nonneg_ring.nonneg a ∨ linear_nonneg_ring.nonneg (-a)

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

source

@[instance]

def nonneg_ring.to_ordered_ring {α : Type u} [nonneg_ring α] :

ordered_ring α

Equations

nonneg_ring.to_ordered_ring = {add := nonneg_ring.add _inst_1, add_assoc := _, zero := nonneg_ring.zero _inst_1, zero_add := _, add_zero := _, neg := nonneg_ring.neg _inst_1, add_left_neg := _, add_comm := _, mul := nonneg_ring.mul _inst_1, mul_assoc := _, one := nonneg_ring.one _inst_1, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, le := ordered_add_comm_group.le infer_instance, lt := ordered_add_comm_group.lt infer_instance, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, exists_pair_ne := _, mul_pos := _}

source

def nonneg_ring.to_linear_nonneg_ring {α : Type u} [nonneg_ring α] :

(∀ (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

nonneg_ring.to_linear_nonneg_ring nonneg_total = {add := nonneg_ring.add _inst_1, add_assoc := _, zero := nonneg_ring.zero _inst_1, zero_add := _, add_zero := _, neg := nonneg_ring.neg _inst_1, add_left_neg := _, add_comm := _, mul := nonneg_ring.mul _inst_1, mul_assoc := _, one := nonneg_ring.one _inst_1, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _, nonneg := nonneg_ring.nonneg _inst_1, pos := nonneg_ring.pos _inst_1, pos_iff := _, zero_nonneg := _, add_nonneg := _, nonneg_antisymm := _, mul_nonneg := _, nonneg_total := nonneg_total}

source

@[instance]

def linear_nonneg_ring.to_nonneg_ring {α : Type u} [linear_nonneg_ring α] :

nonneg_ring α

Equations

linear_nonneg_ring.to_nonneg_ring = {add := linear_nonneg_ring.add _inst_1, add_assoc := _, zero := linear_nonneg_ring.zero _inst_1, zero_add := _, add_zero := _, neg := linear_nonneg_ring.neg _inst_1, add_left_neg := _, add_comm := _, mul := linear_nonneg_ring.mul _inst_1, mul_assoc := _, one := linear_nonneg_ring.one _inst_1, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, nonneg := linear_nonneg_ring.nonneg _inst_1, pos := linear_nonneg_ring.pos _inst_1, pos_iff := _, zero_nonneg := _, add_nonneg := _, nonneg_antisymm := _, exists_pair_ne := _, mul_nonneg := _, mul_pos := _}

source

@[instance]

def linear_nonneg_ring.to_linear_order {α : Type u} [linear_nonneg_ring α] :

linear_order α

Equations

linear_nonneg_ring.to_linear_order = {le := ordered_add_comm_group.le infer_instance, lt := ordered_add_comm_group.lt infer_instance, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _}

source

@[instance]

def linear_nonneg_ring.to_linear_ordered_ring {α : Type u} [linear_nonneg_ring α] :

linear_ordered_ring α

Equations

linear_nonneg_ring.to_linear_ordered_ring = {add := linear_nonneg_ring.add _inst_1, add_assoc := _, zero := linear_nonneg_ring.zero _inst_1, zero_add := _, add_zero := _, neg := linear_nonneg_ring.neg _inst_1, add_left_neg := _, add_comm := _, mul := linear_nonneg_ring.mul _inst_1, mul_assoc := _, one := linear_nonneg_ring.one _inst_1, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, le := ordered_add_comm_group.le infer_instance, lt := ordered_add_comm_group.lt infer_instance, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, exists_pair_ne := _, mul_pos := _, le_total := _, zero_lt_one := _}

source

def linear_nonneg_ring.to_decidable_linear_ordered_comm_ring {α : Type u} [linear_nonneg_ring α] [decidable_pred linear_nonneg_ring.nonneg] [comm : is_commutative α has_mul.mul] :

decidable_linear_ordered_comm_ring α

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

Equations

linear_nonneg_ring.to_decidable_linear_ordered_comm_ring = {add := linear_ordered_ring.add linear_nonneg_ring.to_linear_ordered_ring, add_assoc := _, zero := linear_ordered_ring.zero linear_nonneg_ring.to_linear_ordered_ring, zero_add := _, add_zero := _, neg := linear_ordered_ring.neg linear_nonneg_ring.to_linear_ordered_ring, add_left_neg := _, add_comm := _, mul := linear_ordered_ring.mul linear_nonneg_ring.to_linear_ordered_ring, mul_assoc := _, one := linear_ordered_ring.one linear_nonneg_ring.to_linear_ordered_ring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, le := linear_ordered_ring.le linear_nonneg_ring.to_linear_ordered_ring, lt := linear_ordered_ring.lt linear_nonneg_ring.to_linear_ordered_ring, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, exists_pair_ne := _, mul_pos := _, le_total := _, zero_lt_one := _, mul_comm := _, decidable_le := λ (a b : α), _inst_2 (b - a), decidable_eq := decidable_linear_ordered_add_comm_group.decidable_eq._default linear_ordered_ring.le linear_ordered_ring.lt linear_nonneg_ring.to_decidable_linear_ordered_comm_ring._proof_21 linear_nonneg_ring.to_decidable_linear_ordered_comm_ring._proof_22 linear_nonneg_ring.to_decidable_linear_ordered_comm_ring._proof_23 linear_nonneg_ring.to_decidable_linear_ordered_comm_ring._proof_24 linear_nonneg_ring.to_decidable_linear_ordered_comm_ring._proof_25 (λ (a b : α), _inst_2 (b - a)), decidable_lt := λ (a b : α), decidable_lt_of_decidable_le a b}

source

@[class]

structure canonically_ordered_comm_semiring :

Type u_1 → Type 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 ≤ 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
lt_of_add_lt_add_left : ∀ (a b c_1 : α), a + b < a + c_1 → b < 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
exists_pair_ne : ∃ (x y : α), x ≠ y
eq_zero_or_eq_zero_of_mul_eq_zero : ∀ (a b : α), a * b = 0 → a = 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

source

@[instance]

def canonically_ordered_comm_semiring.to_comm_semiring (α : Type u_1) [s : canonically_ordered_comm_semiring α] :

comm_semiring α

source

@[instance]

def canonically_ordered_comm_semiring.to_nontrivial (α : Type u_1) [s : canonically_ordered_comm_semiring α] :

nontrivial α

source

@[instance]

def canonically_ordered_comm_semiring.to_canonically_ordered_add_monoid (α : Type u_1) [s : canonically_ordered_comm_semiring α] :