Ordered monoids #
This file develops the basics of ordered monoids.
Implementation details #
Unfortunately, the number of ' appended to lemmas in this file
may differ between the multiplicative and the additive version of a lemma.
The reason is that we did not want to change existing names in the library.
@[instance]
@[instance]
@[class]
- 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_monoid.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : α), ordered_comm_monoid.npow n.succ x = x * ordered_comm_monoid.npow n x) . "try_refl_tac"
- 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
An ordered commutative monoid is a commutative monoid with a partial order such that
a ≤ b → c * a ≤ c * b(multiplication is monotone)a * b < a * c → b < c.
@[instance]
@[instance]
@[class]
- 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_add_comm_monoid.nsmul 0 x = 0) . "try_refl_tac"
- nsmul_succ' : (∀ (n : ℕ) (x : α), ordered_add_comm_monoid.nsmul n.succ x = x + ordered_add_comm_monoid.nsmul n x) . "try_refl_tac"
- add_comm : ∀ (a b : α), a + b = b + a
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c_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
An ordered (additive) commutative monoid is a commutative monoid with a partial order such that
a ≤ b → c + a ≤ c + b(addition is monotone)a + b < a + c → b < c.
Instances
- linear_ordered_add_comm_monoid.to_ordered_add_comm_monoid
- canonically_ordered_add_monoid.to_ordered_add_comm_monoid
- ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid
- with_top.ordered_add_comm_monoid
- with_bot.ordered_add_comm_monoid
- order_dual.ordered_add_comm_monoid
- additive.ordered_add_comm_monoid
- rat.ordered_add_comm_monoid
- add_submonoid.to_ordered_add_comm_monoid
- submodule.to_ordered_add_comm_monoid
- enat.ordered_add_comm_monoid
- real.ordered_add_comm_monoid
@[class]
An ordered_comm_monoid with one-sided 'division' in the sense that
if a ≤ b, there is some c for which a * c = b. This is a weaker version
of the condition on canonical orderings defined by canonically_ordered_monoid.
@[class]
An ordered_add_comm_monoid with one-sided 'subtraction' in the sense that
if a ≤ b, then there is some c for which a + c = b. This is a weaker version
of the condition on canonical orderings defined by canonically_ordered_add_monoid.
@[instance]
def
linear_ordered_add_comm_monoid.to_ordered_add_comm_monoid
(α : Type u_1)
[self : linear_ordered_add_comm_monoid α] :
@[instance]
def
linear_ordered_add_comm_monoid.to_linear_order
(α : Type u_1)
[self : linear_ordered_add_comm_monoid α] :
@[class]
- 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
- 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
- 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_add_comm_monoid.nsmul 0 x = 0) . "try_refl_tac"
- nsmul_succ' : (∀ (n : ℕ) (x : α), linear_ordered_add_comm_monoid.nsmul n.succ x = x + linear_ordered_add_comm_monoid.nsmul n x) . "try_refl_tac"
- add_comm : ∀ (a b : α), a + b = b + a
- 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
A linearly ordered additive commutative monoid.
@[class]
- 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
- 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
- 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_comm_monoid.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : α), linear_ordered_comm_monoid.npow n.succ x = x * linear_ordered_comm_monoid.npow n x) . "try_refl_tac"
- mul_comm : ∀ (a b : α), a * b = b * a
- 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
A linearly ordered commutative monoid.
@[instance]
def
linear_ordered_comm_monoid.to_linear_order
(α : Type u_1)
[self : linear_ordered_comm_monoid α] :
@[instance]
def
linear_ordered_comm_monoid.to_ordered_comm_monoid
(α : Type u_1)
[self : linear_ordered_comm_monoid α] :
@[instance]
def
linear_ordered_comm_monoid_with_zero.to_comm_monoid_with_zero
(α : Type u_1)
[self : linear_ordered_comm_monoid_with_zero α] :
@[class]
- 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
- 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
- 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_comm_monoid_with_zero.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : α), linear_ordered_comm_monoid_with_zero.npow n.succ x = x * linear_ordered_comm_monoid_with_zero.npow n x) . "try_refl_tac"
- mul_comm : ∀ (a b : α), a * b = b * a
- 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
- zero : α
- zero_mul : ∀ (a : α), 0 * a = 0
- mul_zero : ∀ (a : α), a * 0 = 0
- zero_le_one : 0 ≤ 1
A linearly ordered commutative monoid with a zero element.
@[instance]
def
linear_ordered_comm_monoid_with_zero.to_linear_ordered_comm_monoid
(α : Type u_1)
[self : linear_ordered_comm_monoid_with_zero α] :
@[instance]
def
linear_ordered_add_comm_monoid_with_top.to_linear_ordered_add_comm_monoid
(α : Type u_1)
[self : linear_ordered_add_comm_monoid_with_top α] :
@[instance]
def
linear_ordered_add_comm_monoid_with_top.to_order_top
(α : Type u_1)
[self : linear_ordered_add_comm_monoid_with_top α] :
@[class]
- 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
- 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
- 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_add_comm_monoid_with_top.nsmul 0 x = 0) . "try_refl_tac"
- nsmul_succ' : (∀ (n : ℕ) (x : α), linear_ordered_add_comm_monoid_with_top.nsmul n.succ x = x + linear_ordered_add_comm_monoid_with_top.nsmul n x) . "try_refl_tac"
- add_comm : ∀ (a b : α), a + b = b + a
- 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
- top : α
- le_top : ∀ (a : α), a ≤ ⊤
- top_add' : ∀ (x : α), ⊤ + x = ⊤
A linearly ordered commutative monoid with an additively absorbing ⊤ element.
Instances should include number systems with an infinite element adjoined.`
theorem
mul_lt_of_mul_lt_left
{α : Type u}
[ordered_comm_monoid α]
{a b c d : α}
(h : a * b < c)
(hle : d ≤ b) :
theorem
add_lt_of_add_lt_left
{α : Type u}
[ordered_add_comm_monoid α]
{a b c d : α}
(h : a + b < c)
(hle : d ≤ b) :
theorem
mul_lt_of_mul_lt_right
{α : Type u}
[ordered_comm_monoid α]
{a b c d : α}
(h : a * b < c)
(hle : d ≤ a) :
theorem
add_lt_of_add_lt_right
{α : Type u}
[ordered_add_comm_monoid α]
{a b c d : α}
(h : a + b < c)
(hle : d ≤ a) :
theorem
add_le_of_add_le_left
{α : Type u}
[ordered_add_comm_monoid α]
{a b c d : α}
(h : a + b ≤ c)
(hle : d ≤ b) :
theorem
mul_le_of_mul_le_left
{α : Type u}
[ordered_comm_monoid α]
{a b c d : α}
(h : a * b ≤ c)
(hle : d ≤ b) :
theorem
mul_le_of_mul_le_right
{α : Type u}
[ordered_comm_monoid α]
{a b c d : α}
(h : a * b ≤ c)
(hle : d ≤ a) :
theorem
add_le_of_add_le_right
{α : Type u}
[ordered_add_comm_monoid α]
{a b c d : α}
(h : a + b ≤ c)
(hle : d ≤ a) :
theorem
lt_add_of_lt_add_left
{α : Type u}
[ordered_add_comm_monoid α]
{a b c d : α}
(h : a < b + c)
(hle : c ≤ d) :
theorem
lt_mul_of_lt_mul_left
{α : Type u}
[ordered_comm_monoid α]
{a b c d : α}
(h : a < b * c)
(hle : c ≤ d) :
theorem
lt_add_of_lt_add_right
{α : Type u}
[ordered_add_comm_monoid α]
{a b c d : α}
(h : a < b + c)
(hle : b ≤ d) :
theorem
lt_mul_of_lt_mul_right
{α : Type u}
[ordered_comm_monoid α]
{a b c d : α}
(h : a < b * c)
(hle : b ≤ d) :
theorem
le_add_of_le_add_left
{α : Type u}
[ordered_add_comm_monoid α]
{a b c d : α}
(h : a ≤ b + c)
(hle : c ≤ d) :
theorem
le_mul_of_le_mul_left
{α : Type u}
[ordered_comm_monoid α]
{a b c d : α}
(h : a ≤ b * c)
(hle : c ≤ d) :
theorem
le_mul_of_le_mul_right
{α : Type u}
[ordered_comm_monoid α]
{a b c d : α}
(h : a ≤ b * c)
(hle : b ≤ d) :
theorem
le_add_of_le_add_right
{α : Type u}
[ordered_add_comm_monoid α]
{a b c d : α}
(h : a ≤ b + c)
(hle : b ≤ d) :
theorem
lt_of_add_lt_add_right
{α : Type u}
[ordered_add_comm_monoid α]
{a b c : α}
(h : a + b < c + b) :
a < c
theorem
lt_of_mul_lt_mul_right'
{α : Type u}
[ordered_comm_monoid α]
{a b c : α}
(h : a * b < c * b) :
a < c
theorem
add_le_add
{α : Type u}
[ordered_add_comm_monoid α]
{a b c d : α}
(h₁ : a ≤ b)
(h₂ : c ≤ d) :
theorem
lt_of_mul_lt_of_one_le_left
{α : Type u}
[ordered_comm_monoid α]
{a b c : α}
(h : a * b < c)
(hle : 1 ≤ b) :
a < c
theorem
lt_of_add_lt_of_nonneg_left
{α : Type u}
[ordered_add_comm_monoid α]
{a b c : α}
(h : a + b < c)
(hle : 0 ≤ b) :
a < c
theorem
lt_of_mul_lt_of_one_le_right
{α : Type u}
[ordered_comm_monoid α]
{a b c : α}
(h : a * b < c)
(hle : 1 ≤ a) :
b < c
theorem
lt_of_add_lt_of_nonneg_right
{α : Type u}
[ordered_add_comm_monoid α]
{a b c : α}
(h : a + b < c)
(hle : 0 ≤ a) :
b < c
theorem
le_of_mul_le_of_one_le_left
{α : Type u}
[ordered_comm_monoid α]
{a b c : α}
(h : a * b ≤ c)
(hle : 1 ≤ b) :
a ≤ c
theorem
le_of_add_le_of_nonneg_left
{α : Type u}
[ordered_add_comm_monoid α]
{a b c : α}
(h : a + b ≤ c)
(hle : 0 ≤ b) :
a ≤ c
theorem
le_of_mul_le_of_one_le_right
{α : Type u}
[ordered_comm_monoid α]
{a b c : α}
(h : a * b ≤ c)
(hle : 1 ≤ a) :
b ≤ c
theorem
le_of_add_le_of_nonneg_right
{α : Type u}
[ordered_add_comm_monoid α]
{a b c : α}
(h : a + b ≤ c)
(hle : 0 ≤ a) :
b ≤ c
theorem
lt_of_lt_add_of_nonpos_left
{α : Type u}
[ordered_add_comm_monoid α]
{a b c : α}
(h : a < b + c)
(hle : c ≤ 0) :
a < b
theorem
lt_of_lt_mul_of_le_one_left
{α : Type u}
[ordered_comm_monoid α]
{a b c : α}
(h : a < b * c)
(hle : c ≤ 1) :
a < b
theorem
lt_of_lt_add_of_nonpos_right
{α : Type u}
[ordered_add_comm_monoid α]
{a b c : α}
(h : a < b + c)
(hle : b ≤ 0) :
a < c
theorem
lt_of_lt_mul_of_le_one_right
{α : Type u}
[ordered_comm_monoid α]
{a b c : α}
(h : a < b * c)
(hle : b ≤ 1) :
a < c
theorem
le_of_le_add_of_nonpos_left
{α : Type u}
[ordered_add_comm_monoid α]
{a b c : α}
(h : a ≤ b + c)
(hle : c ≤ 0) :
a ≤ b
theorem
le_of_le_mul_of_le_one_left
{α : Type u}
[ordered_comm_monoid α]
{a b c : α}
(h : a ≤ b * c)
(hle : c ≤ 1) :
a ≤ b
theorem
le_of_le_mul_of_le_one_right
{α : Type u}
[ordered_comm_monoid α]
{a b c : α}
(h : a ≤ b * c)
(hle : b ≤ 1) :
a ≤ c
theorem
le_of_le_add_of_nonpos_right
{α : Type u}
[ordered_add_comm_monoid α]
{a b c : α}
(h : a ≤ b + c)
(hle : b ≤ 0) :
a ≤ c
theorem
le_add_of_nonneg_of_le
{α : Type u}
[ordered_add_comm_monoid α]
{a b c : α}
(ha : 0 ≤ a)
(hbc : b ≤ c) :
theorem
le_mul_of_one_le_of_le
{α : Type u}
[ordered_comm_monoid α]
{a b c : α}
(ha : 1 ≤ a)
(hbc : b ≤ c) :
theorem
le_add_of_le_of_nonneg
{α : Type u}
[ordered_add_comm_monoid α]
{a b c : α}
(hbc : b ≤ c)
(ha : 0 ≤ a) :
theorem
le_mul_of_le_of_one_le
{α : Type u}
[ordered_comm_monoid α]
{a b c : α}
(hbc : b ≤ c)
(ha : 1 ≤ a) :
theorem
one_lt_mul_of_lt_of_le'
{α : Type u}
[ordered_comm_monoid α]
{a b : α}
(ha : 1 < a)
(hb : 1 ≤ b) :
theorem
add_pos_of_pos_of_nonneg
{α : Type u}
[ordered_add_comm_monoid α]
{a b : α}
(ha : 0 < a)
(hb : 0 ≤ b) :
theorem
add_pos_of_nonneg_of_pos
{α : Type u}
[ordered_add_comm_monoid α]
{a b : α}
(ha : 0 ≤ a)
(hb : 0 < b) :
theorem
one_lt_mul_of_le_of_lt'
{α : Type u}
[ordered_comm_monoid α]
{a b : α}
(ha : 1 ≤ a)
(hb : 1 < b) :
theorem
mul_le_of_le_one_of_le'
{α : Type u}
[ordered_comm_monoid α]
{a b c : α}
(ha : a ≤ 1)
(hbc : b ≤ c) :
theorem
add_le_of_nonpos_of_le'
{α : Type u}
[ordered_add_comm_monoid α]
{a b c : α}
(ha : a ≤ 0)
(hbc : b ≤ c) :
theorem
add_le_of_le_of_nonpos'
{α : Type u}
[ordered_add_comm_monoid α]
{a b c : α}
(hbc : b ≤ c)
(ha : a ≤ 0) :
theorem
mul_le_of_le_of_le_one'
{α : Type u}
[ordered_comm_monoid α]
{a b c : α}
(hbc : b ≤ c)
(ha : a ≤ 1) :
theorem
add_neg_of_neg_of_nonpos'
{α : Type u}
[ordered_add_comm_monoid α]
{a b : α}
(ha : a < 0)
(hb : b ≤ 0) :
theorem
mul_lt_one_of_lt_one_of_le_one'
{α : Type u}
[ordered_comm_monoid α]
{a b : α}
(ha : a < 1)
(hb : b ≤ 1) :
theorem
mul_lt_one_of_le_one_of_lt_one'
{α : Type u}
[ordered_comm_monoid α]
{a b : α}
(ha : a ≤ 1)
(hb : b < 1) :
theorem
add_neg_of_nonpos_of_neg'
{α : Type u}
[ordered_add_comm_monoid α]
{a b : α}
(ha : a ≤ 0)
(hb : b < 0) :
theorem
lt_mul_of_one_le_of_lt'
{α : Type u}
[ordered_comm_monoid α]
{a b c : α}
(ha : 1 ≤ a)
(hbc : b < c) :
theorem
lt_add_of_nonneg_of_lt'
{α : Type u}
[ordered_add_comm_monoid α]
{a b c : α}
(ha : 0 ≤ a)
(hbc : b < c) :
theorem
lt_mul_of_lt_of_one_le'
{α : Type u}
[ordered_comm_monoid α]
{a b c : α}
(hbc : b < c)
(ha : 1 ≤ a) :
theorem
lt_add_of_lt_of_nonneg'
{α : Type u}
[ordered_add_comm_monoid α]
{a b c : α}
(hbc : b < c)
(ha : 0 ≤ a) :
theorem
lt_add_of_pos_of_lt'
{α : Type u}
[ordered_add_comm_monoid α]
{a b c : α}
(ha : 0 < a)
(hbc : b < c) :
theorem
lt_mul_of_one_lt_of_lt'
{α : Type u}
[ordered_comm_monoid α]
{a b c : α}
(ha : 1 < a)
(hbc : b < c) :
theorem
lt_add_of_lt_of_pos'
{α : Type u}
[ordered_add_comm_monoid α]
{a b c : α}
(hbc : b < c)
(ha : 0 < a) :
theorem
lt_mul_of_lt_of_one_lt'
{α : Type u}
[ordered_comm_monoid α]
{a b c : α}
(hbc : b < c)
(ha : 1 < a) :
theorem
add_lt_of_nonpos_of_lt'
{α : Type u}
[ordered_add_comm_monoid α]
{a b c : α}
(ha : a ≤ 0)
(hbc : b < c) :
theorem
mul_lt_of_le_one_of_lt'
{α : Type u}
[ordered_comm_monoid α]
{a b c : α}
(ha : a ≤ 1)
(hbc : b < c) :
theorem
mul_lt_of_lt_of_le_one'
{α : Type u}
[ordered_comm_monoid α]
{a b c : α}
(hbc : b < c)
(ha : a ≤ 1) :
theorem
add_lt_of_lt_of_nonpos'
{α : Type u}
[ordered_add_comm_monoid α]
{a b c : α}
(hbc : b < c)
(ha : a ≤ 0) :
theorem
mul_lt_of_lt_one_of_lt'
{α : Type u}
[ordered_comm_monoid α]
{a b c : α}
(ha : a < 1)
(hbc : b < c) :
theorem
add_lt_of_neg_of_lt'
{α : Type u}
[ordered_add_comm_monoid α]
{a b c : α}
(ha : a < 0)
(hbc : b < c) :
theorem
mul_lt_of_lt_of_lt_one'
{α : Type u}
[ordered_comm_monoid α]
{a b c : α}
(hbc : b < c)
(ha : a < 1) :
theorem
add_lt_of_lt_of_neg'
{α : Type u}
[ordered_add_comm_monoid α]
{a b c : α}
(hbc : b < c)
(ha : a < 0) :
def
function.injective.ordered_comm_monoid
{α : Type u}
[ordered_comm_monoid α]
{β : Type u_1}
[has_one β]
[has_mul β]
(f : β → α)
(hf : function.injective f)
(one : f 1 = 1)
(mul : ∀ (x y : β), f (x * y) = (f x) * f y) :
Pullback an ordered_comm_monoid under an injective map.
Equations
- function.injective.ordered_comm_monoid f hf one mul = {mul := comm_monoid.mul (function.injective.comm_monoid f hf one mul), mul_assoc := _, one := comm_monoid.one (function.injective.comm_monoid f hf one mul), one_mul := _, mul_one := _, npow := comm_monoid.npow (function.injective.comm_monoid f hf one mul), npow_zero' := _, npow_succ' := _, mul_comm := _, le := partial_order.le (partial_order.lift f hf), lt := partial_order.lt (partial_order.lift f hf), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, lt_of_mul_lt_mul_left := _}
def
function.injective.ordered_add_comm_monoid
{α : Type u}
[ordered_add_comm_monoid α]
{β : Type u_1}
[has_zero β]
[has_add β]
(f : β → α)
(hf : function.injective f)
(one : f 0 = 0)
(mul : ∀ (x y : β), f (x + y) = f x + f y) :
Pullback an ordered_add_comm_monoid under an injective map.
theorem
monotone.mul'
{α : Type u}
[ordered_comm_monoid α]
{β : Type u_1}
[preorder β]
{f g : β → α}
(hf : monotone f)
(hg : monotone g) :
theorem
monotone.add
{α : Type u}
[ordered_add_comm_monoid α]
{β : Type u_1}
[preorder β]
{f g : β → α}
(hf : monotone f)
(hg : monotone g) :
theorem
monotone.add_const
{α : Type u}
[ordered_add_comm_monoid α]
{β : Type u_1}
[preorder β]
{f : β → α}
(hf : monotone f)
(a : α) :
theorem
monotone.mul_const'
{α : Type u}
[ordered_comm_monoid α]
{β : Type u_1}
[preorder β]
{f : β → α}
(hf : monotone f)
(a : α) :
theorem
monotone.const_add
{α : Type u}
[ordered_add_comm_monoid α]
{β : Type u_1}
[preorder β]
{f : β → α}
(hf : monotone f)
(a : α) :
theorem
monotone.const_mul'
{α : Type u}
[ordered_comm_monoid α]
{β : Type u_1}
[preorder β]
{f : β → α}
(hf : monotone f)
(a : α) :
def
function.injective.linear_ordered_comm_monoid
{α : Type u}
[linear_ordered_comm_monoid α]
{β : Type u_1}
[has_one β]
[has_mul β]
(f : β → α)
(hf : function.injective f)
(one : f 1 = 1)
(mul : ∀ (x y : β), f (x * y) = (f x) * f y) :
Pullback a linear_ordered_comm_monoid under an injective map.
Equations
- function.injective.linear_ordered_comm_monoid f hf one mul = {le := ordered_comm_monoid.le (function.injective.ordered_comm_monoid f hf one mul), lt := ordered_comm_monoid.lt (function.injective.ordered_comm_monoid f hf one mul), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le (linear_order.lift f hf), decidable_eq := linear_order.decidable_eq (linear_order.lift f hf), decidable_lt := linear_order.decidable_lt (linear_order.lift f hf), mul := ordered_comm_monoid.mul (function.injective.ordered_comm_monoid f hf one mul), mul_assoc := _, one := ordered_comm_monoid.one (function.injective.ordered_comm_monoid f hf one mul), one_mul := _, mul_one := _, npow := ordered_comm_monoid.npow (function.injective.ordered_comm_monoid f hf one mul), npow_zero' := _, npow_succ' := _, mul_comm := _, mul_le_mul_left := _, lt_of_mul_lt_mul_left := _}
def
function.injective.linear_ordered_add_comm_monoid
{α : Type u}
[linear_ordered_add_comm_monoid α]
{β : Type u_1}
[has_zero β]
[has_add β]
(f : β → α)
(hf : function.injective f)
(one : f 0 = 0)
(mul : ∀ (x y : β), f (x + y) = f x + f y) :
Pullback an ordered_add_comm_monoid under an injective map.
@[protected, instance]
@[protected, instance]
Equations
@[simp, norm_cast]
@[simp, norm_cast]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[simp, norm_cast]
@[simp, norm_cast]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp, norm_cast]
@[simp, norm_cast]
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem
with_zero.lt_of_mul_lt_mul_left
{α : Type u}
[ordered_comm_monoid α]
(a b c : with_zero α) :
@[protected, instance]
Equations
- with_zero.ordered_comm_monoid = {mul := comm_monoid_with_zero.mul with_zero.comm_monoid_with_zero, mul_assoc := _, one := comm_monoid_with_zero.one with_zero.comm_monoid_with_zero, one_mul := _, mul_one := _, npow := comm_monoid_with_zero.npow with_zero.comm_monoid_with_zero, npow_zero' := _, npow_succ' := _, mul_comm := _, le := partial_order.le with_zero.partial_order, lt := partial_order.lt with_zero.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, lt_of_mul_lt_mul_left := _}
def
with_zero.ordered_add_comm_monoid
{α : Type u}
[ordered_add_comm_monoid α]
(zero_le : ∀ (a : α), 0 ≤ a) :
If 0 is the least element in α, then with_zero α is an ordered_add_comm_monoid.
Equations
- with_zero.ordered_add_comm_monoid zero_le = {add := add_comm_monoid.add with_zero.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero with_zero.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul with_zero.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := partial_order.le with_zero.partial_order, lt := partial_order.lt with_zero.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, lt_of_add_lt_add_left := _}
@[protected, instance]
Equations
- with_top.has_one = {one := ↑1}
@[protected, instance]
@[protected, instance]
Equations
- with_top.has_add = {add := λ (o₁ o₂ : with_top α), option.bind o₁ (λ (a : α), option.map (λ (b : α), a + b) o₂)}
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
- with_top.add_monoid = {add := has_add.add with_top.has_add, add_assoc := _, zero := some 0, zero_add := _, add_zero := _, nsmul := nsmul additive.add_monoid, nsmul_zero' := _, nsmul_succ' := _}
@[protected, instance]
Equations
- with_top.add_comm_monoid = {add := has_add.add with_top.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul additive.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
@[protected, instance]
Equations
- with_top.ordered_add_comm_monoid = {add := add_comm_monoid.add with_top.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero with_top.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul with_top.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := partial_order.le with_top.partial_order, lt := partial_order.lt with_top.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, lt_of_add_lt_add_left := _}
@[protected, instance]
def
with_top.linear_ordered_add_comm_monoid_with_top
{α : Type u}
[linear_ordered_add_comm_monoid α] :
Equations
- with_top.linear_ordered_add_comm_monoid_with_top = {le := order_top.le with_top.order_top, lt := order_top.lt with_top.order_top, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le with_top.linear_order, decidable_eq := linear_order.decidable_eq with_top.linear_order, decidable_lt := linear_order.decidable_lt with_top.linear_order, 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 := _, nsmul := ordered_add_comm_monoid.nsmul with_top.ordered_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, add_le_add_left := _, lt_of_add_lt_add_left := _, top := order_top.top with_top.order_top, le_top := _, top_add' := _}
Coercion from α to with_top α as an add_monoid_hom.
Equations
- with_top.coe_add_hom = {to_fun := coe coe_to_lift, map_zero' := _, map_add' := _}
@[simp]
@[simp, norm_cast]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations
- with_bot.ordered_add_comm_monoid = {add := add_comm_monoid.add with_bot.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero with_bot.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul with_bot.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := partial_order.le with_bot.partial_order, lt := partial_order.lt with_bot.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, lt_of_add_lt_add_left := _}
@[simp]
@[simp]
@[instance]
def
canonically_ordered_add_monoid.to_ordered_add_comm_monoid
(α : Type u_1)
[self : canonically_ordered_add_monoid α] :
@[instance]
def
canonically_ordered_add_monoid.to_order_bot
(α : Type u_1)
[self : canonically_ordered_add_monoid α] :
@[class]
- 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 : α), canonically_ordered_add_monoid.nsmul 0 x = 0) . "try_refl_tac"
- nsmul_succ' : (∀ (n : ℕ) (x : α), canonically_ordered_add_monoid.nsmul n.succ x = x + canonically_ordered_add_monoid.nsmul n x) . "try_refl_tac"
- add_comm : ∀ (a b : α), a + b = b + a
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c_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
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
- canonically_linear_ordered_add_monoid.to_canonically_ordered_add_monoid
- canonically_ordered_comm_semiring.to_canonically_ordered_add_monoid
- with_zero.canonically_ordered_add_monoid
- with_top.canonically_ordered_add_monoid
- multiset.canonically_ordered_add_monoid
- enat.canonically_ordered_add_monoid
- finsupp.canonically_ordered_add_monoid
- punit.canonically_ordered_add_monoid
- prime_multiset.canonically_ordered_add_monoid
@[instance]
@[instance]
def
canonically_ordered_monoid.to_ordered_comm_monoid
(α : Type u_1)
[self : canonically_ordered_monoid α] :
@[class]
- 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 : α), canonically_ordered_monoid.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : α), canonically_ordered_monoid.npow n.succ x = x * canonically_ordered_monoid.npow n x) . "try_refl_tac"
- 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).
@[simp]
@[simp]
@[simp]
@[simp]
theorem
exists_pos_add_of_lt
{α : Type u}
[canonically_ordered_add_monoid α]
{a b : α}
(h : a < b) :
@[protected, instance]
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 := _, nsmul := ordered_add_comm_monoid.nsmul (with_zero.ordered_add_comm_monoid zero_le), nsmul_zero' := _, nsmul_succ' := _, 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 := _}
@[protected, instance]
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 := _, nsmul := ordered_add_comm_monoid.nsmul with_top.ordered_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, 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 := _}
@[protected, instance]
@[protected, instance]
def
canonically_ordered_add_monoid.has_exists_add_of_le
(α : Type u)
[canonically_ordered_add_monoid α] :
@[instance]
def
canonically_linear_ordered_add_monoid.to_linear_order
(α : Type u_1)
[self : canonically_linear_ordered_add_monoid α] :
@[instance]
def
canonically_linear_ordered_add_monoid.to_canonically_ordered_add_monoid
(α : Type u_1)
[self : canonically_linear_ordered_add_monoid α] :
@[class]
- 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 : α), canonically_linear_ordered_add_monoid.nsmul 0 x = 0) . "try_refl_tac"
- nsmul_succ' : (∀ (n : ℕ) (x : α), canonically_linear_ordered_add_monoid.nsmul n.succ x = x + canonically_linear_ordered_add_monoid.nsmul n x) . "try_refl_tac"
- add_comm : ∀ (a b : α), a + b = b + a
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c_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.
@[instance]
def
canonically_linear_ordered_monoid.to_linear_order
(α : Type u_1)
[self : canonically_linear_ordered_monoid α] :
@[instance]
def
canonically_linear_ordered_monoid.to_canonically_ordered_monoid
(α : Type u_1)
[self : canonically_linear_ordered_monoid α] :
@[class]
- 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 : α), canonically_linear_ordered_monoid.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : α), canonically_linear_ordered_monoid.npow n.succ x = x * canonically_linear_ordered_monoid.npow n x) . "try_refl_tac"
- 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.
@[protected, instance]
@[protected, instance]
def
canonically_linear_ordered_monoid.semilattice_sup_bot
{α : Type u}
[canonically_linear_ordered_monoid α] :
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 := _}
@[protected, instance]
def
with_top.canonically_linear_ordered_add_monoid
(α : Type u_1)
[canonically_linear_ordered_add_monoid α] :
Equations
- with_top.canonically_linear_ordered_add_monoid α = {add := canonically_ordered_add_monoid.add infer_instance, add_assoc := _, zero := canonically_ordered_add_monoid.zero infer_instance, zero_add := _, add_zero := _, nsmul := canonically_ordered_add_monoid.nsmul infer_instance, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := canonically_ordered_add_monoid.le infer_instance, lt := canonically_ordered_add_monoid.lt infer_instance, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, lt_of_add_lt_add_left := _, bot := canonically_ordered_add_monoid.bot infer_instance, bot_le := _, le_iff_exists_add := _, le_total := _, decidable_le := linear_order.decidable_le infer_instance, decidable_eq := linear_order.decidable_eq infer_instance, decidable_lt := linear_order.decidable_lt infer_instance}
@[class]
- 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
- nsmul : ℕ → α → α
- nsmul_zero' : (∀ (x : α), ordered_cancel_add_comm_monoid.nsmul 0 x = 0) . "try_refl_tac"
- nsmul_succ' : (∀ (n : ℕ) (x : α), ordered_cancel_add_comm_monoid.nsmul n.succ x = x + ordered_cancel_add_comm_monoid.nsmul n x) . "try_refl_tac"
- add_comm : ∀ (a b : α), a + b = b + a
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c_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
- linear_ordered_cancel_add_comm_monoid.to_ordered_cancel_add_comm_monoid
- ordered_add_comm_group.to_ordered_cancel_add_comm_monoid
- ordered_semiring.to_ordered_cancel_add_comm_monoid
- order_dual.ordered_cancel_add_comm_monoid
- prod.ordered_cancel_add_comm_monoid
- additive.ordered_cancel_add_comm_monoid
- multiset.ordered_cancel_add_comm_monoid
- rat.ordered_cancel_add_comm_monoid
- add_submonoid.to_ordered_cancel_add_comm_monoid
- submodule.to_ordered_cancel_add_comm_monoid
- finsupp.ordered_cancel_add_comm_monoid
- pi.ordered_cancel_add_comm_monoid
- real.ordered_cancel_add_comm_monoid
- filter.germ.ordered_cancel_add_comm_monoid
- num.ordered_cancel_add_comm_monoid
@[instance]
def
ordered_cancel_add_comm_monoid.to_add_cancel_comm_monoid
(α : Type u)
[self : ordered_cancel_add_comm_monoid α] :
@[instance]
def
ordered_cancel_add_comm_monoid.to_partial_order
(α : Type u)
[self : ordered_cancel_add_comm_monoid α] :
@[instance]
def
ordered_cancel_comm_monoid.to_partial_order
(α : Type u)
[self : ordered_cancel_comm_monoid α] :
@[instance]
def
ordered_cancel_comm_monoid.to_cancel_comm_monoid
(α : Type u)
[self : ordered_cancel_comm_monoid α] :
@[class]
- 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
- npow : ℕ → α → α
- npow_zero' : (∀ (x : α), ordered_cancel_comm_monoid.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : α), ordered_cancel_comm_monoid.npow n.succ x = x * ordered_cancel_comm_monoid.npow n x) . "try_refl_tac"
- 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
- 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
- linear_ordered_cancel_comm_monoid.to_ordered_cancel_comm_monoid
- ordered_comm_group.to_ordered_cancel_comm_monoid
- order_dual.ordered_cancel_comm_monoid
- prod.ordered_cancel_comm_monoid
- multiplicative.ordered_cancel_comm_monoid
- pnat.ordered_cancel_comm_monoid
- submonoid.to_ordered_cancel_comm_monoid
- pi.ordered_cancel_comm_monoid
- filter.germ.ordered_cancel_comm_monoid
@[protected, instance]
@[protected, instance]
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 := _, npow := ordered_cancel_comm_monoid.npow _inst_1, npow_zero' := _, npow_succ' := _, 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 := _}
theorem
add_lt_add_left
{α : Type u}
[ordered_cancel_add_comm_monoid α]
{a b : α}
(h : a < b)
(c : α) :
theorem
mul_lt_mul_left'
{α : Type u}
[ordered_cancel_comm_monoid α]
{a b : α}
(h : a < b)
(c : α) :
theorem
mul_lt_mul_right'
{α : Type u}
[ordered_cancel_comm_monoid α]
{a b : α}
(h : a < b)
(c : α) :
theorem
add_lt_add_right
{α : Type u}
[ordered_cancel_add_comm_monoid α]
{a b : α}
(h : a < b)
(c : α) :
theorem
mul_lt_mul'''
{α : Type u}
[ordered_cancel_comm_monoid α]
{a b c d : α}
(h₁ : a < b)
(h₂ : c < d) :
theorem
add_lt_add
{α : Type u}
[ordered_cancel_add_comm_monoid α]
{a b c d : α}
(h₁ : a < b)
(h₂ : c < d) :
theorem
mul_lt_mul_of_le_of_lt
{α : Type u}
[ordered_cancel_comm_monoid α]
{a b c d : α}
(h₁ : a ≤ b)
(h₂ : c < d) :
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) :
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) :
theorem
mul_lt_mul_of_lt_of_le
{α : Type u}
[ordered_cancel_comm_monoid α]
{a b c d : α}
(h₁ : a < b)
(h₂ : c ≤ d) :
theorem
lt_add_of_pos_right
{α : Type u}
[ordered_cancel_add_comm_monoid α]
(a : α)
{b : α}
(h : 0 < b) :
theorem
lt_mul_of_one_lt_right'
{α : Type u}
[ordered_cancel_comm_monoid α]
(a : α)
{b : α}
(h : 1 < b) :
theorem
lt_add_of_pos_left
{α : Type u}
[ordered_cancel_add_comm_monoid α]
(a : α)
{b : α}
(h : 0 < b) :
theorem
lt_mul_of_one_lt_left'
{α : Type u}
[ordered_cancel_comm_monoid α]
(a : α)
{b : α}
(h : 1 < b) :
theorem
le_of_mul_le_mul_right'
{α : Type u}
[ordered_cancel_comm_monoid α]
{a b c : α}
(h : a * b ≤ c * b) :
a ≤ c
theorem
le_of_add_le_add_right
{α : Type u}
[ordered_cancel_add_comm_monoid α]
{a b c : α}
(h : a + b ≤ c + b) :
a ≤ c
theorem
mul_lt_one
{α : Type u}
[ordered_cancel_comm_monoid α]
{a b : α}
(ha : a < 1)
(hb : b < 1) :
theorem
add_neg_of_neg_of_nonpos
{α : Type u}
[ordered_cancel_add_comm_monoid α]
{a b : α}
(ha : a < 0)
(hb : b ≤ 0) :
theorem
mul_lt_one_of_lt_one_of_le_one
{α : Type u}
[ordered_cancel_comm_monoid α]
{a b : α}
(ha : a < 1)
(hb : b ≤ 1) :
theorem
mul_lt_one_of_le_one_of_lt_one
{α : Type u}
[ordered_cancel_comm_monoid α]
{a b : α}
(ha : a ≤ 1)
(hb : b < 1) :
theorem
add_neg_of_nonpos_of_neg
{α : Type u}
[ordered_cancel_add_comm_monoid α]
{a b : α}
(ha : a ≤ 0)
(hb : b < 0) :
theorem
lt_add_of_pos_of_le
{α : Type u}
[ordered_cancel_add_comm_monoid α]
{a b c : α}
(ha : 0 < a)
(hbc : b ≤ c) :
theorem
lt_mul_of_one_lt_of_le
{α : Type u}
[ordered_cancel_comm_monoid α]
{a b c : α}
(ha : 1 < a)
(hbc : b ≤ c) :
theorem
lt_add_of_le_of_pos
{α : Type u}
[ordered_cancel_add_comm_monoid α]
{a b c : α}
(hbc : b ≤ c)
(ha : 0 < a) :
theorem
lt_mul_of_le_of_one_lt
{α : Type u}
[ordered_cancel_comm_monoid α]
{a b c : α}
(hbc : b ≤ c)
(ha : 1 < a) :
theorem
add_le_of_nonpos_of_le
{α : Type u}
[ordered_cancel_add_comm_monoid α]
{a b c : α}
(ha : a ≤ 0)
(hbc : b ≤ c) :
theorem
mul_le_of_le_one_of_le
{α : Type u}
[ordered_cancel_comm_monoid α]
{a b c : α}
(ha : a ≤ 1)
(hbc : b ≤ c) :
theorem
mul_le_of_le_of_le_one
{α : Type u}
[ordered_cancel_comm_monoid α]
{a b c : α}
(hbc : b ≤ c)
(ha : a ≤ 1) :
theorem
add_le_of_le_of_nonpos
{α : Type u}
[ordered_cancel_add_comm_monoid α]
{a b c : α}
(hbc : b ≤ c)
(ha : a ≤ 0) :
theorem
mul_lt_of_lt_one_of_le
{α : Type u}
[ordered_cancel_comm_monoid α]
{a b c : α}
(ha : a < 1)
(hbc : b ≤ c) :
theorem
add_lt_of_neg_of_le
{α : Type u}
[ordered_cancel_add_comm_monoid α]
{a b c : α}
(ha : a < 0)
(hbc : b ≤ c) :
theorem
add_lt_of_le_of_neg
{α : Type u}
[ordered_cancel_add_comm_monoid α]
{a b c : α}
(hbc : b ≤ c)
(ha : a < 0) :
theorem
mul_lt_of_le_of_lt_one
{α : Type u}
[ordered_cancel_comm_monoid α]
{a b c : α}
(hbc : b ≤ c)
(ha : a < 1) :
theorem
lt_mul_of_one_le_of_lt
{α : Type u}
[ordered_cancel_comm_monoid α]
{a b c : α}
(ha : 1 ≤ a)
(hbc : b < c) :
theorem
lt_add_of_nonneg_of_lt
{α : Type u}
[ordered_cancel_add_comm_monoid α]
{a b c : α}
(ha : 0 ≤ a)
(hbc : b < c) :
theorem
lt_mul_of_lt_of_one_le
{α : Type u}
[ordered_cancel_comm_monoid α]
{a b c : α}
(hbc : b < c)
(ha : 1 ≤ a) :
theorem
lt_add_of_lt_of_nonneg
{α : Type u}
[ordered_cancel_add_comm_monoid α]
{a b c : α}
(hbc : b < c)
(ha : 0 ≤ a) :
theorem
lt_mul_of_one_lt_of_lt
{α : Type u}
[ordered_cancel_comm_monoid α]
{a b c : α}
(ha : 1 < a)
(hbc : b < c) :
theorem
lt_add_of_pos_of_lt
{α : Type u}
[ordered_cancel_add_comm_monoid α]
{a b c : α}
(ha : 0 < a)
(hbc : b < c) :
theorem
lt_mul_of_lt_of_one_lt
{α : Type u}
[ordered_cancel_comm_monoid α]
{a b c : α}
(hbc : b < c)
(ha : 1 < a) :
theorem
lt_add_of_lt_of_pos
{α : Type u}
[ordered_cancel_add_comm_monoid α]
{a b c : α}
(hbc : b < c)
(ha : 0 < a) :
theorem
mul_lt_of_le_one_of_lt
{α : Type u}
[ordered_cancel_comm_monoid α]
{a b c : α}
(ha : a ≤ 1)
(hbc : b < c) :
theorem
add_lt_of_nonpos_of_lt
{α : Type u}
[ordered_cancel_add_comm_monoid α]
{a b c : α}
(ha : a ≤ 0)
(hbc : b < c) :
theorem
add_lt_of_lt_of_nonpos
{α : Type u}
[ordered_cancel_add_comm_monoid α]
{a b c : α}
(hbc : b < c)
(ha : a ≤ 0) :
theorem
mul_lt_of_lt_of_le_one
{α : Type u}
[ordered_cancel_comm_monoid α]
{a b c : α}
(hbc : b < c)
(ha : a ≤ 1) :
theorem
add_lt_of_neg_of_lt
{α : Type u}
[ordered_cancel_add_comm_monoid α]
{a b c : α}
(ha : a < 0)
(hbc : b < c) :
theorem
mul_lt_of_lt_one_of_lt
{α : Type u}
[ordered_cancel_comm_monoid α]
{a b c : α}
(ha : a < 1)
(hbc : b < c) :
theorem
mul_lt_of_lt_of_lt_one
{α : Type u}
[ordered_cancel_comm_monoid α]
{a b c : α}
(hbc : b < c)
(ha : a < 1) :
theorem
add_lt_of_lt_of_neg
{α : Type u}
[ordered_cancel_add_comm_monoid α]
{a b c : α}
(hbc : b < c)
(ha : a < 0) :
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
def
function.injective.ordered_cancel_add_comm_monoid
{α : Type u}
[ordered_cancel_add_comm_monoid α]
{β : Type u_1}
[has_zero β]
[has_add β]
(f : β → α)
(hf : function.injective f)
(one : f 0 = 0)
(mul : ∀ (x y : β), f (x + y) = f x + f y) :
Pullback an ordered_cancel_add_comm_monoid under an injective map.
def
function.injective.ordered_cancel_comm_monoid
{α : Type u}
[ordered_cancel_comm_monoid α]
{β : Type u_1}
[has_one β]
[has_mul β]
(f : β → α)
(hf : function.injective f)
(one : f 1 = 1)
(mul : ∀ (x y : β), f (x * y) = (f x) * f y) :
Pullback an ordered_cancel_comm_monoid under an injective map.
Equations
- function.injective.ordered_cancel_comm_monoid f hf one mul = {mul := left_cancel_semigroup.mul (function.injective.left_cancel_semigroup f hf mul), mul_assoc := _, mul_left_cancel := _, one := ordered_comm_monoid.one (function.injective.ordered_comm_monoid f hf one mul), one_mul := _, mul_one := _, npow := ordered_comm_monoid.npow (function.injective.ordered_comm_monoid f hf one mul), npow_zero' := _, npow_succ' := _, mul_comm := _, le := ordered_comm_monoid.le (function.injective.ordered_comm_monoid f hf one mul), lt := ordered_comm_monoid.lt (function.injective.ordered_comm_monoid f hf one mul), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_of_mul_le_mul_left := _}
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)
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)
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)
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)
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)
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)
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)
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)
Some lemmas about types that have an ordering and a binary operation, with no rules relating them.
theorem
fn_min_mul_fn_max
{α : Type u}
{β : Type u_1}
[linear_order α]
[comm_semigroup β]
(f : α → β)
(n m : α) :
theorem
fn_min_add_fn_max
{α : Type u}
{β : Type u_1}
[linear_order α]
[add_comm_semigroup β]
(f : α → β)
(n m : α) :
@[class]
- 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
- nsmul : ℕ → α → α
- nsmul_zero' : (∀ (x : α), linear_ordered_cancel_add_comm_monoid.nsmul 0 x = 0) . "try_refl_tac"
- nsmul_succ' : (∀ (n : ℕ) (x : α), linear_ordered_cancel_add_comm_monoid.nsmul n.succ x = x + linear_ordered_cancel_add_comm_monoid.nsmul n x) . "try_refl_tac"
- add_comm : ∀ (a b : α), a + b = b + a
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c_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
- lt_of_add_lt_add_left : ∀ (a b c_1 : α), a + b < a + c_1 → b < c_1
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
- linear_ordered_add_comm_group.to_linear_ordered_cancel_add_comm_monoid
- order_dual.linear_ordered_cancel_add_comm_monoid
- nat.linear_ordered_cancel_add_comm_monoid
- add_submonoid.to_linear_ordered_cancel_add_comm_monoid
- submodule.to_linear_ordered_cancel_add_comm_monoid
- punit.linear_ordered_cancel_add_comm_monoid
@[instance]
@[instance]
@[instance]
def
linear_ordered_cancel_comm_monoid.to_linear_ordered_comm_monoid
(α : Type u)
[self : linear_ordered_cancel_comm_monoid α] :
@[instance]
def
linear_ordered_cancel_comm_monoid.to_ordered_cancel_comm_monoid
(α : Type u)
[self : linear_ordered_cancel_comm_monoid α] :
@[class]
- 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
- npow : ℕ → α → α
- npow_zero' : (∀ (x : α), linear_ordered_cancel_comm_monoid.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : α), linear_ordered_cancel_comm_monoid.npow n.succ x = x * linear_ordered_cancel_comm_monoid.npow n x) . "try_refl_tac"
- 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
- le_of_mul_le_mul_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
- lt_of_mul_lt_mul_left : ∀ (a b c_1 : α), a * b < a * c_1 → b < c_1
A linearly ordered cancellative commutative monoid is a commutative monoid with a linear order in which multiplication is cancellative and monotone.
theorem
min_le_add_of_nonneg_right
{α : Type u}
[linear_ordered_cancel_add_comm_monoid α]
{a b : α}
(hb : 0 ≤ b) :
theorem
min_le_mul_of_one_le_right
{α : Type u}
[linear_ordered_cancel_comm_monoid α]
{a b : α}
(hb : 1 ≤ b) :
theorem
min_le_add_of_nonneg_left
{α : Type u}
[linear_ordered_cancel_add_comm_monoid α]
{a b : α}
(ha : 0 ≤ a) :
theorem
min_le_mul_of_one_le_left
{α : Type u}
[linear_ordered_cancel_comm_monoid α]
{a b : α}
(ha : 1 ≤ a) :
theorem
max_le_mul_of_one_le
{α : Type u}
[linear_ordered_cancel_comm_monoid α]
{a b : α}
(ha : 1 ≤ a)
(hb : 1 ≤ b) :
theorem
max_le_add_of_nonneg
{α : Type u}
[linear_ordered_cancel_add_comm_monoid α]
{a b : α}
(ha : 0 ≤ a)
(hb : 0 ≤ b) :
def
function.injective.linear_ordered_cancel_comm_monoid
{α : Type u}
[linear_ordered_cancel_comm_monoid α]
{β : Type u_1}
[has_one β]
[has_mul β]
(f : β → α)
(hf : function.injective f)
(one : f 1 = 1)
(mul : ∀ (x y : β), f (x * y) = (f x) * f y) :
Pullback a linear_ordered_cancel_comm_monoid under an injective map.
Equations
- function.injective.linear_ordered_cancel_comm_monoid f hf one mul = {mul := linear_ordered_comm_monoid.mul (function.injective.linear_ordered_comm_monoid f hf one mul), mul_assoc := _, mul_left_cancel := _, one := linear_ordered_comm_monoid.one (function.injective.linear_ordered_comm_monoid f hf one mul), one_mul := _, mul_one := _, npow := linear_ordered_comm_monoid.npow (function.injective.linear_ordered_comm_monoid f hf one mul), npow_zero' := _, npow_succ' := _, mul_comm := _, le := linear_ordered_comm_monoid.le (function.injective.linear_ordered_comm_monoid f hf one mul), lt := linear_ordered_comm_monoid.lt (function.injective.linear_ordered_comm_monoid f hf one mul), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_of_mul_le_mul_left := _, le_total := _, decidable_le := linear_ordered_comm_monoid.decidable_le (function.injective.linear_ordered_comm_monoid f hf one mul), decidable_eq := linear_ordered_comm_monoid.decidable_eq (function.injective.linear_ordered_comm_monoid f hf one mul), decidable_lt := linear_ordered_comm_monoid.decidable_lt (function.injective.linear_ordered_comm_monoid f hf one mul), lt_of_mul_lt_mul_left := _}
def
function.injective.linear_ordered_cancel_add_comm_monoid
{α : Type u}
[linear_ordered_cancel_add_comm_monoid α]
{β : Type u_1}
[has_zero β]
[has_add β]
(f : β → α)
(hf : function.injective f)
(one : f 0 = 0)
(mul : ∀ (x y : β), f (x + y) = f x + f y) :
Pullback a linear_ordered_cancel_add_comm_monoid under an injective map.
@[protected, instance]
@[protected, instance]
Equations
- order_dual.ordered_comm_monoid = {mul := comm_monoid.mul (show comm_monoid α, from ordered_comm_monoid.to_comm_monoid α), mul_assoc := _, one := comm_monoid.one (show comm_monoid α, from ordered_comm_monoid.to_comm_monoid α), one_mul := _, mul_one := _, npow := comm_monoid.npow (show comm_monoid α, from ordered_comm_monoid.to_comm_monoid α), npow_zero' := _, npow_succ' := _, mul_comm := _, le := partial_order.le (order_dual.partial_order α), lt := partial_order.lt (order_dual.partial_order α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, lt_of_mul_lt_mul_left := _}
@[protected, instance]
Equations
- order_dual.ordered_cancel_comm_monoid = {mul := ordered_comm_monoid.mul order_dual.ordered_comm_monoid, mul_assoc := _, mul_left_cancel := _, one := ordered_comm_monoid.one order_dual.ordered_comm_monoid, one_mul := _, mul_one := _, npow := ordered_comm_monoid.npow order_dual.ordered_comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, le := ordered_comm_monoid.le order_dual.ordered_comm_monoid, lt := ordered_comm_monoid.lt order_dual.ordered_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_of_mul_le_mul_left := _}
@[protected, instance]
@[protected, instance]
def
order_dual.linear_ordered_cancel_comm_monoid
{α : Type u}
[linear_ordered_cancel_comm_monoid α] :
Equations
- order_dual.linear_ordered_cancel_comm_monoid = {mul := ordered_cancel_comm_monoid.mul order_dual.ordered_cancel_comm_monoid, mul_assoc := _, mul_left_cancel := _, one := ordered_cancel_comm_monoid.one order_dual.ordered_cancel_comm_monoid, one_mul := _, mul_one := _, npow := ordered_cancel_comm_monoid.npow order_dual.ordered_cancel_comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, le := linear_order.le (order_dual.linear_order α), lt := linear_order.lt (order_dual.linear_order α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_of_mul_le_mul_left := _, le_total := _, decidable_le := linear_order.decidable_le (order_dual.linear_order α), decidable_eq := linear_order.decidable_eq (order_dual.linear_order α), decidable_lt := linear_order.decidable_lt (order_dual.linear_order α), lt_of_mul_lt_mul_left := _}
@[protected, instance]
@[protected, instance]
def
prod.ordered_cancel_comm_monoid
{M : Type u_1}
{N : Type u_2}
[ordered_cancel_comm_monoid M]
[ordered_cancel_comm_monoid N] :
ordered_cancel_comm_monoid (M × N)
Equations
- prod.ordered_cancel_comm_monoid = {mul := cancel_comm_monoid.mul prod.cancel_comm_monoid, mul_assoc := _, mul_left_cancel := _, one := cancel_comm_monoid.one prod.cancel_comm_monoid, one_mul := _, mul_one := _, npow := cancel_comm_monoid.npow prod.cancel_comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, le := partial_order.le (prod.partial_order M N), lt := partial_order.lt (prod.partial_order M N), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_of_mul_le_mul_left := _}
@[protected, instance]
def
prod.ordered_cancel_add_comm_monoid
{M : Type u_1}
{N : Type u_2}
[ordered_cancel_add_comm_monoid M]
[ordered_cancel_add_comm_monoid N] :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
- multiplicative.ordered_comm_monoid = {mul := comm_monoid.mul multiplicative.comm_monoid, mul_assoc := _, one := comm_monoid.one multiplicative.comm_monoid, one_mul := _, mul_one := _, npow := comm_monoid.npow multiplicative.comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, le := partial_order.le multiplicative.partial_order, lt := partial_order.lt multiplicative.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, lt_of_mul_lt_mul_left := _}
@[protected, instance]
Equations
- additive.ordered_add_comm_monoid = {add := add_comm_monoid.add additive.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero additive.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul additive.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := partial_order.le additive.partial_order, lt := partial_order.lt additive.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, lt_of_add_lt_add_left := _}
@[protected, instance]
Equations
- multiplicative.ordered_cancel_comm_monoid = {mul := left_cancel_semigroup.mul multiplicative.left_cancel_semigroup, mul_assoc := _, mul_left_cancel := _, one := ordered_comm_monoid.one multiplicative.ordered_comm_monoid, one_mul := _, mul_one := _, npow := ordered_comm_monoid.npow multiplicative.ordered_comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, le := ordered_comm_monoid.le multiplicative.ordered_comm_monoid, lt := ordered_comm_monoid.lt multiplicative.ordered_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_of_mul_le_mul_left := _}
@[protected, instance]
Equations
- additive.ordered_cancel_add_comm_monoid = {add := add_left_cancel_semigroup.add additive.add_left_cancel_semigroup, add_assoc := _, add_left_cancel := _, zero := ordered_add_comm_monoid.zero additive.ordered_add_comm_monoid, zero_add := _, add_zero := _, nsmul := ordered_add_comm_monoid.nsmul additive.ordered_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := ordered_add_comm_monoid.le additive.ordered_add_comm_monoid, lt := ordered_add_comm_monoid.lt additive.ordered_add_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _}
@[protected, instance]
Equations
- multiplicative.linear_ordered_comm_monoid = {le := linear_order.le multiplicative.linear_order, lt := linear_order.lt multiplicative.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le multiplicative.linear_order, decidable_eq := linear_order.decidable_eq multiplicative.linear_order, decidable_lt := linear_order.decidable_lt multiplicative.linear_order, mul := ordered_comm_monoid.mul multiplicative.ordered_comm_monoid, mul_assoc := _, one := ordered_comm_monoid.one multiplicative.ordered_comm_monoid, one_mul := _, mul_one := _, npow := ordered_comm_monoid.npow multiplicative.ordered_comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, mul_le_mul_left := _, lt_of_mul_lt_mul_left := _}
@[protected, instance]
Equations
- additive.linear_ordered_add_comm_monoid = {le := linear_order.le additive.linear_order, lt := linear_order.lt additive.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le additive.linear_order, decidable_eq := linear_order.decidable_eq additive.linear_order, decidable_lt := linear_order.decidable_lt additive.linear_order, add := ordered_add_comm_monoid.add additive.ordered_add_comm_monoid, add_assoc := _, zero := ordered_add_comm_monoid.zero additive.ordered_add_comm_monoid, zero_add := _, add_zero := _, nsmul := ordered_add_comm_monoid.nsmul additive.ordered_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, add_le_add_left := _, lt_of_add_lt_add_left := _}
@[protected, instance]
Equations
- order_dual.sub_neg_monoid = {add := sub_neg_monoid.add (show sub_neg_monoid α, from _inst_1), add_assoc := _, zero := sub_neg_monoid.zero (show sub_neg_monoid α, from _inst_1), zero_add := _, add_zero := _, nsmul := sub_neg_monoid.nsmul (show sub_neg_monoid α, from _inst_1), nsmul_zero' := _, nsmul_succ' := _, neg := sub_neg_monoid.neg (show sub_neg_monoid α, from _inst_1), sub := sub_neg_monoid.sub (show sub_neg_monoid α, from _inst_1), sub_eq_add_neg := _, gsmul := gsmul (show sub_neg_monoid α, from _inst_1), gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _}
@[protected, instance]
Equations
- order_dual.div_inv_monoid = {mul := div_inv_monoid.mul (show div_inv_monoid α, from _inst_1), mul_assoc := _, one := div_inv_monoid.one (show div_inv_monoid α, from _inst_1), one_mul := _, mul_one := _, npow := div_inv_monoid.npow (show div_inv_monoid α, from _inst_1), npow_zero' := _, npow_succ' := _, inv := div_inv_monoid.inv (show div_inv_monoid α, from _inst_1), div := div_inv_monoid.div (show div_inv_monoid α, from _inst_1), div_eq_mul_inv := _, gpow := gpow (show div_inv_monoid α, from _inst_1), gpow_zero' := _, gpow_succ' := _, gpow_neg' := _}