mathlib docs: algebra.ordered

A canonically ordered additive monoid is an ordered commutative additive monoid in which the ordering coincides with the subtractibility relation, which is to say, 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 nontrivial ordered_add_comm_groups.

Instances

source

@[instance]

def canonically_ordered_monoid.to_order_bot (α : Type u_1) [s : canonically_ordered_monoid α] :

order_bot α

source

@[instance]

def canonically_ordered_monoid.to_ordered_comm_monoid (α : Type u_1) [s : canonically_ordered_monoid α] :

ordered_comm_monoid α

source

@[class]

structure canonically_ordered_monoid (α : Type u_1) :

Type u_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
mul_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
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 * a ≤ c_1 * b
lt_of_mul_lt_mul_left : ∀ (a b c_1 : α), a * b < a * c_1 → b < c_1
bot : α
bot_le : ∀ (a : α), ⊥ ≤ a
le_iff_exists_mul : ∀ (a b : α), a ≤ b ↔ ∃ (c_1 : α), b = a * c_1

A canonically ordered monoid is an ordered commutative monoid in which the ordering coincides with the divisibility relation, which is to say, a ≤ b iff there exists c with b = a * c. Example seem rare; it seems more likely that the order_dual of a naturally-occurring lattice satisfies this than the lattice itself (for example, dual of the lattice of ideals of a PID or Dedekind domain satisfy this; collections of all things ≤ 1 seem to be more natural that collections of all things ≥ 1).

Instances

canonically_linear_ordered_monoid.to_canonically_ordered_monoid

source

theorem le_iff_exists_add {α : Type u} [canonically_ordered_add_monoid α] {a b : α} :

a ≤ b ↔ ∃ (c : α), b = a + c

source

theorem le_iff_exists_mul {α : Type u} [canonically_ordered_monoid α] {a b : α} :

a ≤ b ↔ ∃ (c : α), b = a * c

source

theorem self_le_mul_right {α : Type u} [canonically_ordered_monoid α] (a b : α) :

a ≤ a * b

source

theorem self_le_add_right {α : Type u} [canonically_ordered_add_monoid α] (a b : α) :

a ≤ a + b

source

theorem self_le_add_left {α : Type u} [canonically_ordered_add_monoid α] (a b : α) :

a ≤ b + a

source

theorem self_le_mul_left {α : Type u} [canonically_ordered_monoid α] (a b : α) :

a ≤ b * a

source

@[simp]

theorem one_le {α : Type u} [canonically_ordered_monoid α] (a : α) :

1 ≤ a

source

@[simp]

theorem zero_le {α : Type u} [canonically_ordered_add_monoid α] (a : α) :

0 ≤ a

source

@[simp]

theorem bot_eq_one {α : Type u} [canonically_ordered_monoid α] :

⊥ = 1

source

@[simp]

theorem bot_eq_zero {α : Type u} [canonically_ordered_add_monoid α] :

⊥ = 0

source

@[simp]

theorem mul_eq_one_iff {α : Type u} [canonically_ordered_monoid α] {a b : α} :

a * b = 1 ↔ a = 1 ∧ b = 1

source

@[simp]

theorem add_eq_zero_iff {α : Type u} [canonically_ordered_add_monoid α] {a b : α} :

a + b = 0 ↔ a = 0 ∧ b = 0

source

@[simp]

theorem le_one_iff_eq_one {α : Type u} [canonically_ordered_monoid α] {a : α} :

a ≤ 1 ↔ a = 1

source

@[simp]

theorem nonpos_iff_eq_zero {α : Type u} [canonically_ordered_add_monoid α] {a : α} :

a ≤ 0 ↔ a = 0

source

theorem one_lt_iff_ne_one {α : Type u} [canonically_ordered_monoid α] {a : α} :

1 < a ↔ a ≠ 1

source

theorem pos_iff_ne_zero {α : Type u} [canonically_ordered_add_monoid α] {a : α} :

0 < a ↔ a ≠ 0

source

theorem exists_pos_mul_of_lt {α : Type u} [canonically_ordered_monoid α] {a b : α} (h : a < b) :

∃ (c : α) (H : c > 1), a * c = b

source

theorem exists_pos_add_of_lt {α : Type u} [canonically_ordered_add_monoid α] {a b : α} (h : a < b) :

∃ (c : α) (H : c > 0), a + c = b

source

theorem le_add_left {α : Type u} [canonically_ordered_add_monoid α] {a b c : α} (h : a ≤ c) :

a ≤ b + c

source

theorem le_mul_left {α : Type u} [canonically_ordered_monoid α] {a b c : α} (h : a ≤ c) :

a ≤ b * c

source

theorem le_add_right {α : Type u} [canonically_ordered_add_monoid α] {a b c : α} (h : a ≤ b) :

a ≤ b + c

source

theorem le_mul_right {α : Type u} [canonically_ordered_monoid α] {a b c : α} (h : a ≤ b) :

a ≤ b * c

source

@[instance]

def with_zero.canonically_ordered_add_monoid {α : Type u} [canonically_ordered_add_monoid α] :

canonically_ordered_add_monoid (with_zero α)

Adding a new zero to a canonically ordered additive monoid produces another one.

Equations

with_zero.canonically_ordered_add_monoid = {add := ordered_add_comm_monoid.add (with_zero.ordered_add_comm_monoid zero_le), add_assoc := _, zero := ordered_add_comm_monoid.zero (with_zero.ordered_add_comm_monoid zero_le), zero_add := _, add_zero := _, add_comm := _, le := ordered_add_comm_monoid.le (with_zero.ordered_add_comm_monoid zero_le), lt := ordered_add_comm_monoid.lt (with_zero.ordered_add_comm_monoid zero_le), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, lt_of_add_lt_add_left := _, bot := 0, bot_le := _, le_iff_exists_add := _}

source

@[instance]

def with_top.canonically_ordered_add_monoid {α : Type u} [canonically_ordered_add_monoid α] :

canonically_ordered_add_monoid (with_top α)

Equations

with_top.canonically_ordered_add_monoid = {add := ordered_add_comm_monoid.add with_top.ordered_add_comm_monoid, add_assoc := _, zero := ordered_add_comm_monoid.zero with_top.ordered_add_comm_monoid, zero_add := _, add_zero := _, add_comm := _, le := order_bot.le with_top.order_bot, lt := order_bot.lt with_top.order_bot, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, lt_of_add_lt_add_left := _, bot := order_bot.bot with_top.order_bot, bot_le := _, le_iff_exists_add := _}

source

@[instance]

def canonically_linear_ordered_add_monoid.to_linear_order (α : Type u_1) [s : canonically_linear_ordered_add_monoid α] :

linear_order α

source

@[instance]

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

canonically_ordered_add_monoid α

source

@[class]

structure canonically_linear_ordered_add_monoid (α : 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
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

A canonically linear-ordered additive monoid is a canonically ordered additive monoid whose ordering is a linear order.

source

@[instance]

def canonically_linear_ordered_monoid.to_linear_order (α : Type u_1) [s : canonically_linear_ordered_monoid α] :

linear_order α

source

@[instance]

def canonically_linear_ordered_monoid.to_canonically_ordered_monoid (α : Type u_1) [s : canonically_linear_ordered_monoid α] :

canonically_ordered_monoid α

source

@[class]

structure canonically_linear_ordered_monoid (α : Type u_1) :

Type u_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
mul_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
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 * a ≤ c_1 * b
lt_of_mul_lt_mul_left : ∀ (a b c_1 : α), a * b < a * c_1 → b < c_1
bot : α
bot_le : ∀ (a : α), ⊥ ≤ a
le_iff_exists_mul : ∀ (a b : α), a ≤ b ↔ ∃ (c_1 : α), b = a * 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

A canonically linear-ordered monoid is a canonically ordered monoid whose ordering is a linear order.

source

@[instance]

def canonically_linear_ordered_add_monoid.semilattice_sup_bot {α : Type u} [canonically_linear_ordered_add_monoid α] :

semilattice_sup_bot α

source

@[instance]

def canonically_linear_ordered_monoid.semilattice_sup_bot {α : Type u} [canonically_linear_ordered_monoid α] :

semilattice_sup_bot α

Equations

canonically_linear_ordered_monoid.semilattice_sup_bot = {bot := order_bot.bot (canonically_ordered_monoid.to_order_bot α), le := lattice.le lattice_of_linear_order, lt := lattice.lt lattice_of_linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, sup := lattice.sup lattice_of_linear_order, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[class]

structure ordered_cancel_add_comm_monoid (α : Type u) :

Type u

add : α → α → α
add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
add_left_cancel : ∀ (a b c_1 : α), a + b = a + c_1 → b = c_1
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
add_comm : ∀ (a b : α), a + b = b + a
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

An ordered cancellative additive commutative monoid is an additive commutative monoid with a partial order, in which addition is cancellative and monotone.

Instances

source

@[instance]

def ordered_cancel_add_comm_monoid.to_add_cancel_comm_monoid (α : Type u) [s : ordered_cancel_add_comm_monoid α] :

add_cancel_comm_monoid α

source

@[instance]

def ordered_cancel_add_comm_monoid.to_partial_order (α : Type u) [s : ordered_cancel_add_comm_monoid α] :

partial_order α

source

@[instance]

def ordered_cancel_comm_monoid.to_partial_order (α : Type u) [s : ordered_cancel_comm_monoid α] :

partial_order α

source

@[instance]

def ordered_cancel_comm_monoid.to_cancel_comm_monoid (α : Type u) [s : ordered_cancel_comm_monoid α] :

cancel_comm_monoid α

source

@[class]

structure ordered_cancel_comm_monoid (α : Type u) :

Type u

mul : α → α → α
mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
mul_left_cancel : ∀ (a b c_1 : α), a * b = a * c_1 → b = c_1
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
mul_comm : ∀ (a b : α), a * b = b * a
mul_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
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 * a ≤ c_1 * b
le_of_mul_le_mul_left : ∀ (a b c_1 : α), a * b ≤ a * c_1 → b ≤ c_1

An ordered cancellative commutative monoid is a commutative monoid with a partial order, in which multiplication is cancellative and monotone.

Instances

source

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

a * b ≤ a * c → b ≤ c

source

theorem le_of_add_le_add_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :

a + b ≤ a + c → b ≤ c

source

@[instance]

def ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid {α : Type u} [ordered_cancel_add_comm_monoid α] :

ordered_add_comm_monoid α

source

@[instance]

def ordered_cancel_comm_monoid.to_ordered_comm_monoid {α : Type u} [ordered_cancel_comm_monoid α] :

ordered_comm_monoid α

Equations

ordered_cancel_comm_monoid.to_ordered_comm_monoid = {mul := ordered_cancel_comm_monoid.mul _inst_1, mul_assoc := _, one := ordered_cancel_comm_monoid.one _inst_1, one_mul := _, mul_one := _, mul_comm := _, le := ordered_cancel_comm_monoid.le _inst_1, lt := ordered_cancel_comm_monoid.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, lt_of_mul_lt_mul_left := _}

source

theorem add_lt_add_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (h : a < b) (c : α) :

c + a < c + b

source

theorem mul_lt_mul_left' {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} (h : a < b) (c : α) :

c * a < c * b

source

theorem mul_lt_mul_right' {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} (h : a < b) (c : α) :

a * c < b * c

source

theorem add_lt_add_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (h : a < b) (c : α) :

a + c < b + c

source

theorem mul_lt_mul''' {α : Type u} [ordered_cancel_comm_monoid α] {a b c d : α} (h₁ : a < b) (h₂ : c < d) :

a * c < b * d

source

theorem add_lt_add {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c d : α} (h₁ : a < b) (h₂ : c < d) :

a + c < b + d

source

theorem mul_lt_mul_of_le_of_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c d : α} (h₁ : a ≤ b) (h₂ : c < d) :

a * c < b * d

source

theorem add_lt_add_of_le_of_lt {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c d : α} (h₁ : a ≤ b) (h₂ : c < d) :

a + c < b + d

source

theorem add_lt_add_of_lt_of_le {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c d : α} (h₁ : a < b) (h₂ : c ≤ d) :

a + c < b + d

source

theorem mul_lt_mul_of_lt_of_le {α : Type u} [ordered_cancel_comm_monoid α] {a b c d : α} (h₁ : a < b) (h₂ : c ≤ d) :

a * c < b * d

source

theorem lt_add_of_pos_right {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b : α} (h : 0 < b) :

a < a + b

source

theorem lt_mul_of_one_lt_right' {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b : α} (h : 1 < b) :

a < a * b

source

theorem lt_add_of_pos_left {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b : α} (h : 0 < b) :

a < b + a

source

theorem lt_mul_of_one_lt_left' {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b : α} (h : 1 < b) :

a < b * a

source

theorem le_of_mul_le_mul_right' {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (h : a * b ≤ c * b) :

a ≤ c

source

theorem le_of_add_le_add_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (h : a + b ≤ c + b) :

a ≤ c

source

theorem mul_lt_one {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} (ha : a < 1) (hb : b < 1) :

a * b < 1

source

theorem add_neg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (ha : a < 0) (hb : b < 0) :

a + b < 0

source

theorem add_neg_of_neg_of_nonpos {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (ha : a < 0) (hb : b ≤ 0) :

a + b < 0

source

theorem mul_lt_one_of_lt_one_of_le_one {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} (ha : a < 1) (hb : b ≤ 1) :

a * b < 1

source

theorem mul_lt_one_of_le_one_of_lt_one {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} (ha : a ≤ 1) (hb : b < 1) :

a * b < 1

source

theorem add_neg_of_nonpos_of_neg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (ha : a ≤ 0) (hb : b < 0) :

a + b < 0

source

theorem lt_add_of_pos_of_le {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (ha : 0 < a) (hbc : b ≤ c) :

b < a + c

source

theorem lt_mul_of_one_lt_of_le {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (ha : 1 < a) (hbc : b ≤ c) :

b < a * c

source

theorem lt_add_of_le_of_pos {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (hbc : b ≤ c) (ha : 0 < a) :

b < c + a

source

theorem lt_mul_of_le_of_one_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (hbc : b ≤ c) (ha : 1 < a) :

b < c * a

source

theorem add_le_of_nonpos_of_le {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (ha : a ≤ 0) (hbc : b ≤ c) :

a + b ≤ c

source

theorem mul_le_of_le_one_of_le {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (ha : a ≤ 1) (hbc : b ≤ c) :

a * b ≤ c

source

theorem mul_le_of_le_of_le_one {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (hbc : b ≤ c) (ha : a ≤ 1) :

b * a ≤ c

source

theorem add_le_of_le_of_nonpos {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (hbc : b ≤ c) (ha : a ≤ 0) :

b + a ≤ c

source

theorem mul_lt_of_lt_one_of_le {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (ha : a < 1) (hbc : b ≤ c) :

a * b < c

source

theorem add_lt_of_neg_of_le {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (ha : a < 0) (hbc : b ≤ c) :

a + b < c

source

theorem add_lt_of_le_of_neg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (hbc : b ≤ c) (ha : a < 0) :

b + a < c

source

theorem mul_lt_of_le_of_lt_one {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (hbc : b ≤ c) (ha : a < 1) :

b * a < c

source

theorem lt_mul_of_one_le_of_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (ha : 1 ≤ a) (hbc : b < c) :

b < a * c

source

theorem lt_add_of_nonneg_of_lt {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (ha : 0 ≤ a) (hbc : b < c) :

b < a + c

source

theorem lt_mul_of_lt_of_one_le {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (hbc : b < c) (ha : 1 ≤ a) :

b < c * a

source

theorem lt_add_of_lt_of_nonneg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (hbc : b < c) (ha : 0 ≤ a) :

b < c + a

source

theorem lt_mul_of_one_lt_of_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (ha : 1 < a) (hbc : b < c) :

b < a * c

source

theorem lt_add_of_pos_of_lt {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (ha : 0 < a) (hbc : b < c) :

b < a + c

source

theorem lt_mul_of_lt_of_one_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (hbc : b < c) (ha : 1 < a) :

b < c * a

source

theorem lt_add_of_lt_of_pos {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (hbc : b < c) (ha : 0 < a) :

b < c + a

source

theorem mul_lt_of_le_one_of_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (ha : a ≤ 1) (hbc : b < c) :

a * b < c

source

theorem add_lt_of_nonpos_of_lt {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (ha : a ≤ 0) (hbc : b < c) :

a + b < c

source

theorem add_lt_of_lt_of_nonpos {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (hbc : b < c) (ha : a ≤ 0) :

b + a < c

source

theorem mul_lt_of_lt_of_le_one {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (hbc : b < c) (ha : a ≤ 1) :

b * a < c

source

theorem add_lt_of_neg_of_lt {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (ha : a < 0) (hbc : b < c) :

a + b < c

source

theorem mul_lt_of_lt_one_of_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (ha : a < 1) (hbc : b < c) :

a * b < c

source

theorem mul_lt_of_lt_of_lt_one {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (hbc : b < c) (ha : a < 1) :

b * a < c

source

theorem add_lt_of_lt_of_neg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (hbc : b < c) (ha : a < 0) :

b + a < c

source

@[simp]

theorem mul_le_mul_iff_left {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b c : α} :

a * b ≤ a * c ↔ b ≤ c

source

@[simp]

theorem add_le_add_iff_left {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b c : α} :

a + b ≤ a + c ↔ b ≤ c

source

@[simp]

theorem mul_le_mul_iff_right {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} (c : α) :

a * c ≤ b * c ↔ a ≤ b

source

@[simp]

theorem add_le_add_iff_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (c : α) :

a + c ≤ b + c ↔ a ≤ b

source

@[simp]

theorem mul_lt_mul_iff_left {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b c : α} :

a * b < a * c ↔ b < c

source

@[simp]

theorem add_lt_add_iff_left {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b c : α} :

a + b < a + c ↔ b < c

source

@[simp]

theorem mul_lt_mul_iff_right {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} (c : α) :

a * c < b * c ↔ a < b

source

@[simp]

theorem add_lt_add_iff_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (c : α) :

a + c < b + c ↔ a < b

source

@[simp]

theorem le_add_iff_nonneg_right {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b : α} :

a ≤ a + b ↔ 0 ≤ b

source

@[simp]

theorem le_mul_iff_one_le_right' {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b : α} :

a ≤ a * b ↔ 1 ≤ b

source

@[simp]

theorem le_add_iff_nonneg_left {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b : α} :

a ≤ b + a ↔ 0 ≤ b

source

@[simp]

theorem le_mul_iff_one_le_left' {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b : α} :

a ≤ b * a ↔ 1 ≤ b

source

@[simp]

theorem lt_add_iff_pos_right {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b : α} :

a < a + b ↔ 0 < b

source

@[simp]

theorem lt_mul_iff_one_lt_right' {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b : α} :

a < a * b ↔ 1 < b

source

@[simp]

theorem lt_add_iff_pos_left {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b : α} :

a < b + a ↔ 0 < b

source

@[simp]

theorem lt_mul_iff_one_lt_left' {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b : α} :

a < b * a ↔ 1 < b

source

@[simp]

theorem add_le_iff_nonpos_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} :

a + b ≤ b ↔ a ≤ 0

source

@[simp]

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

a * b ≤ b ↔ a ≤ 1

source

@[simp]

theorem add_le_iff_nonpos_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} :

a + b ≤ a ↔ b ≤ 0

source

@[simp]

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

a * b ≤ a ↔ b ≤ 1

source

@[simp]

theorem add_lt_iff_neg_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} :

a + b < b ↔ a < 0

source

@[simp]

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

a * b < b ↔ a < 1

source

@[simp]

theorem add_lt_iff_neg_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} :

a + b < a ↔ b < 0

source

@[simp]

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

a * b < a ↔ b < 1

source

theorem mul_eq_one_iff_eq_one_of_one_le {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) :

a * b = 1 ↔ a = 1 ∧ b = 1

source

theorem add_eq_zero_iff_eq_zero_of_nonneg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) :

a + b = 0 ↔ a = 0 ∧ b = 0

source

theorem monotone.mul_strict_mono' {α : Type u} [ordered_cancel_comm_monoid α] {β : Type u_1} [preorder β] {f g : β → α} (hf : monotone f) (hg : strict_mono g) :

strict_mono (λ (x : β), (f x) * g x)

source

theorem monotone.add_strict_mono {α : Type u} [ordered_cancel_add_comm_monoid α] {β : Type u_1} [preorder β] {f g : β → α} (hf : monotone f) (hg : strict_mono g) :

strict_mono (λ (x : β), f x + g x)

source

theorem strict_mono.add_monotone {α : Type u} [ordered_cancel_add_comm_monoid α] {β : Type u_1} [preorder β] {f g : β → α} (hf : strict_mono f) (hg : monotone g) :

strict_mono (λ (x : β), f x + g x)

source

theorem strict_mono.mul_monotone' {α : Type u} [ordered_cancel_comm_monoid α] {β : Type u_1} [preorder β] {f g : β → α} (hf : strict_mono f) (hg : monotone g) :

strict_mono (λ (x : β), (f x) * g x)

source

theorem strict_mono.add_const {α : Type u} [ordered_cancel_add_comm_monoid α] {β : Type u_1} [preorder β] {f : β → α} (hf : strict_mono f) (c : α) :

strict_mono (λ (x : β), f x + c)

source

theorem strict_mono.mul_const' {α : Type u} [ordered_cancel_comm_monoid α] {β : Type u_1} [preorder β] {f : β → α} (hf : strict_mono f) (c : α) :

strict_mono (λ (x : β), (f x) * c)

source

theorem strict_mono.const_add {α : Type u} [ordered_cancel_add_comm_monoid α] {β : Type u_1} [preorder β] {f : β → α} (hf : strict_mono f) (c : α) :

strict_mono (λ (x : β), c + f x)

source

theorem strict_mono.const_mul' {α : Type u} [ordered_cancel_comm_monoid α] {β : Type u_1} [preorder β] {f : β → α} (hf : strict_mono f) (c : α) :

strict_mono (λ (x : β), c * f x)

source

theorem with_top.add_lt_add_iff_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : with_top α} :

a < ⊤ → (a + c < a + b ↔ c < b)

source

theorem with_bot.add_lt_add_iff_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : with_bot α} :

⊥ < a → (a + c < a + b ↔ c < b)

source

theorem with_top.add_lt_add_iff_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : with_top α} :

a < ⊤ → (c + a < b + a ↔ c < b)

source

theorem with_bot.add_lt_add_iff_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : with_bot α} :

⊥ < a → (c + a < b + a ↔ c < b)

source

theorem fn_min_mul_fn_max {α : Type u} {β : Type u_1} [linear_order α] [comm_semigroup β] (f : α → β) (n m : α) :

(f (min n m)) * f (max n m) = (f n) * f m

source

theorem fn_min_add_fn_max {α : Type u} {β : Type u_1} [linear_order α] [add_comm_semigroup β] (f : α → β) (n m : α) :

f (min n m) + f (max n m) = f n + f m

source

theorem min_add_max {α : Type u} [linear_order α] [add_comm_semigroup α] (n m : α) :

min n m + max n m = n + m

source

theorem min_mul_max {α : Type u} [linear_order α] [comm_semigroup α] (n m : α) :

(min n m) * max n m = n * m

source

@[class]

structure linear_ordered_cancel_add_comm_monoid (α : Type u) :

Type u

add : α → α → α
add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
add_left_cancel : ∀ (a b c_1 : α), a + b = a + c_1 → b = c_1
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
add_comm : ∀ (a b : α), a + b = b + a
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
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

A linearly ordered cancellative additive commutative monoid is an additive commutative monoid with a decidable linear order in which addition is cancellative and monotone.

Instances

source

@[instance]

def linear_ordered_cancel_add_comm_monoid.to_linear_order (α : Type u) [s : linear_ordered_cancel_add_comm_monoid α] :

linear_order α

source

@[instance]

def linear_ordered_cancel_add_comm_monoid.to_ordered_cancel_add_comm_monoid (α : Type u) [s : linear_ordered_cancel_add_comm_monoid α] :

ordered_cancel_add_comm_monoid α

source

@[instance]

def linear_ordered_cancel_comm_monoid.to_linear_order (α : Type u) [s : linear_ordered_cancel_comm_monoid α] :