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.
- 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
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
.
- 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
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
- 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
- enat.ordered_add_comm_monoid
- real.ordered_add_comm_monoid
- 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
- mul_comm : ∀ (a b : α), a * b = b * a
- zero : α
- zero_mul : ∀ (a : α), 0 * a = 0
- mul_zero : ∀ (a : α), a * 0 = 0
- 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_le_one : 0 ≤ 1
A linearly ordered commutative monoid with a zero element.
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
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 := _, 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 := _}
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 := _, 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 := _}
Equations
- with_top.has_one = {one := ↑1}
Equations
- with_top.has_add = {add := λ (o₁ o₂ : with_top α), option.bind o₁ (λ (a : α), option.map (λ (b : α), a + b) o₂)}
Equations
Equations
- with_top.add_monoid = {add := has_add.add with_top.has_add, add_assoc := _, zero := some 0, zero_add := _, add_zero := _}
Equations
- with_top.add_comm_monoid = {add := has_add.add with_top.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, add_comm := _}
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 := _, 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 := _}
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' := _}
Equations
Equations
Equations
Equations
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 := _, 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 := _}
- 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
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_group
s.
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
- nnreal.canonically_ordered_add_monoid
- prime_multiset.canonically_ordered_add_monoid
- 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).
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 := _}
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 := _}
- 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.
- 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.
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 := _}
- 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
- 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
- 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
- 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
- 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
- pi.ordered_cancel_comm_monoid
- filter.germ.ordered_cancel_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 := _}
Some lemmas about types that have an ordering and a binary operation, with no rules relating them.
- 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.
- 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
- 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 commutative monoid is a commutative monoid with a linear order in which multiplication is cancellative and monotone.
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 := _, 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 := _}
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 := _, mul_comm := _, mul_right_cancel := _, 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 := _}
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 := _, mul_comm := _, mul_right_cancel := _, 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 α)}
Equations
- prod.ordered_cancel_comm_monoid = {mul := comm_monoid.mul prod.comm_monoid, mul_assoc := _, mul_left_cancel := _, one := comm_monoid.one prod.comm_monoid, one_mul := _, mul_one := _, mul_comm := _, mul_right_cancel := _, 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 := _}
Equations
Equations
Equations
Equations
Equations
Equations
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 := _, 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 := _}
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 := _, 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 := _}
Equations
- multiplicative.ordered_cancel_comm_monoid = {mul := right_cancel_semigroup.mul multiplicative.right_cancel_semigroup, mul_assoc := _, mul_left_cancel := _, one := ordered_comm_monoid.one multiplicative.ordered_comm_monoid, one_mul := _, mul_one := _, mul_comm := _, mul_right_cancel := _, 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 := _}
Equations
- additive.ordered_cancel_add_comm_monoid = {add := add_right_cancel_semigroup.add additive.add_right_cancel_semigroup, add_assoc := _, add_left_cancel := _, zero := ordered_add_comm_monoid.zero additive.ordered_add_comm_monoid, zero_add := _, add_zero := _, add_comm := _, add_right_cancel := _, 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 := _}