• mul : α → α → α
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• 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 : α), a ≤ b → b ≤ c → a ≤ c
• 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 : α), c * a ≤ c * b

An ordered commutative monoid is a commutative monoid with a partial order such that a ≤ b → c * a ≤ c * b (multiplication is monotone)

Instances of this typeclass

• submonoid_class.to_ordered_comm_monoid
• linear_ordered_comm_monoid.to_ordered_comm_monoid
• ordered_cancel_comm_monoid.to_ordered_comm_monoid
• canonically_ordered_monoid.to_ordered_comm_monoid
• canonically_ordered_comm_semiring.to_ordered_comm_monoid
• with_zero.ordered_comm_monoid
• order_dual.ordered_comm_monoid
• multiplicative.ordered_comm_monoid
• associates.ordered_comm_monoid
• submonoid.to_ordered_comm_monoid
• positive.subtype.ordered_comm_monoid
• prod.ordered_comm_monoid
• pi.ordered_comm_monoid
• filter.germ.ordered_comm_monoid

Instances of other typeclasses for ordered_comm_monoid

• ordered_comm_monoid.has_sizeof_inst

• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• 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 : α), a ≤ b → b ≤ c → a ≤ c
• 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 : α), c + a ≤ c + b

An ordered (additive) commutative monoid is a commutative monoid with a partial order such that a ≤ b → c + a ≤ c + b (addition is monotone)

Instances of this typeclass

• add_submonoid_class.to_ordered_add_comm_monoid
• linear_ordered_add_comm_monoid.to_ordered_add_comm_monoid
• ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid
• canonically_ordered_add_monoid.to_ordered_add_comm_monoid
• ordered_semiring.to_ordered_add_comm_monoid
• star_ordered_ring.to_ordered_add_comm_monoid
• order_dual.ordered_add_comm_monoid
• with_top.ordered_add_comm_monoid
• with_bot.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
• prod.ordered_add_comm_monoid
• part_enat.ordered_add_comm_monoid
• finsupp.ordered_add_comm_monoid
• pi.ordered_add_comm_monoid
• nonneg.ordered_add_comm_monoid
• real.ordered_add_comm_monoid
• dfinsupp.ordered_add_comm_monoid
• filter.germ.ordered_add_comm_monoid

Instances of other typeclasses for ordered_add_comm_monoid

• ordered_add_comm_monoid.has_sizeof_inst

• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• 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
• max : α → α → α
• max_def : linear_ordered_add_comm_monoid.max = max_default . "reflexivity"
• min : α → α → α
• min_def : linear_ordered_add_comm_monoid.min = min_default . "reflexivity"
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• 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 : α), c + a ≤ c + b

A linearly ordered additive commutative monoid.

Instances of this typeclass

• add_submonoid_class.to_linear_ordered_add_comm_monoid
• linear_ordered_add_comm_monoid_with_top.to_linear_ordered_add_comm_monoid
• linear_ordered_cancel_add_comm_monoid.to_linear_ordered_add_comm_monoid
• linear_ordered_semiring.to_linear_ordered_add_comm_monoid
• order_dual.linear_ordered_add_comm_monoid
• with_bot.linear_ordered_add_comm_monoid
• additive.linear_ordered_add_comm_monoid
• add_submonoid.to_linear_ordered_add_comm_monoid
• submodule.to_linear_ordered_add_comm_monoid
• nonneg.linear_ordered_add_comm_monoid
• ereal.linear_ordered_add_comm_monoid
• counterexample.counterexample_not_prime_but_homogeneous_prime.two.linear_ordered_add_comm_monoid

Instances of other typeclasses for linear_ordered_add_comm_monoid

• linear_ordered_add_comm_monoid.has_sizeof_inst

• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• 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
• max : α → α → α
• max_def : linear_ordered_comm_monoid.max = max_default . "reflexivity"
• min : α → α → α
• min_def : linear_ordered_comm_monoid.min = min_default . "reflexivity"
• mul : α → α → α
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• 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 : α), c * a ≤ c * b

A linearly ordered commutative monoid.

Instances of this typeclass

• submonoid_class.to_linear_ordered_comm_monoid
• linear_ordered_cancel_comm_monoid.to_linear_ordered_comm_monoid
• linear_ordered_comm_monoid_with_zero.to_linear_ordered_comm_monoid
• order_dual.linear_ordered_comm_monoid
• multiplicative.linear_ordered_comm_monoid
• submonoid.to_linear_ordered_comm_monoid

Instances of other typeclasses for linear_ordered_comm_monoid

• linear_ordered_comm_monoid.has_sizeof_inst

• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• 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
• max : α → α → α
• max_def : linear_ordered_add_comm_monoid_with_top.max = max_default . "reflexivity"
• min : α → α → α
• min_def : linear_ordered_add_comm_monoid_with_top.min = min_default . "reflexivity"
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• 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 : α), c + a ≤ c + b
• top : α
• le_top : ∀ (x : α), x ≤ ⊤
• top_add' : ∀ (x : α), ⊤ + x = ⊤

A linearly ordered commutative monoid with an additively absorbing ⊤ element. Instances should include number systems with an infinite element adjoined.`

Instances of this typeclass

• linear_ordered_add_comm_group_with_top.to_linear_ordered_add_comm_monoid_with_top
• with_top.linear_ordered_add_comm_monoid_with_top
• additive.linear_ordered_add_comm_monoid_with_top
• punit.linear_ordered_add_comm_monoid_with_top
• enat.linear_ordered_add_comm_monoid_with_top
• part_enat.linear_ordered_add_comm_monoid_with_top
• ennreal.linear_ordered_add_comm_monoid_with_top

Instances of other typeclasses for linear_ordered_add_comm_monoid_with_top

• linear_ordered_add_comm_monoid_with_top.has_sizeof_inst