• 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_with_zero.max = max_default . "reflexivity"
• min : α → α → α
• min_def : linear_ordered_comm_monoid_with_zero.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_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 : α), c * a ≤ c * b
• 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.

Instances of this typeclass

• linear_ordered_comm_group_with_zero.to_linear_ordered_comm_monoid_with_zero
• nat.linear_ordered_comm_monoid_with_zero
• multiplicative.linear_ordered_comm_monoid_with_zero
• with_zero.linear_ordered_comm_monoid_with_zero
• cardinal.linear_ordered_comm_monoid_with_zero
• nonneg.linear_ordered_comm_monoid_with_zero
• ennreal.linear_ordered_comm_monoid_with_zero

Instances of other typeclasses for linear_ordered_comm_monoid_with_zero

• linear_ordered_comm_monoid_with_zero.has_sizeof_inst