Documentation

Mathlib.Algebra.Order.Monoid.WithZero.Defs

Adjoining a zero element to an ordered monoid. #

class LinearOrderedCommMonoidWithZero (α : Type u_1) extends , :
Type u_1
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• min : ααα
• max : ααα
• compare : ααOrdering
• le_total : ∀ (a b : α), a b b a
• decidableLE : DecidableRel fun x x_1 => x x_1
• decidableEq :
• decidableLT : DecidableRel fun x x_1 => x < x_1
• min_def : ∀ (a b : α), min a b = if a b then a else b
• max_def : ∀ (a b : α), max a b = if a b then b else a
• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b =
• 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 : α), = 1
• npow_succ : ∀ (n : ) (x : α), Monoid.npow (n + 1) x = x *
• 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

Zero is a left absorbing element for multiplication

• mul_zero : ∀ (a : α), a * 0 = 0

Zero is a right absorbing element for multiplication

• zero_le_one : 0 1

0 ≤ 1 in any linearly ordered commutative monoid.

A linearly ordered commutative monoid with a zero element.

Instances
instance WithZero.preorder {α : Type u} [] :
instance WithZero.partialOrder {α : Type u} [] :
instance WithZero.orderBot {α : Type u} [] :
theorem WithZero.zero_le {α : Type u} [] (a : ) :
0 a
theorem WithZero.zero_lt_coe {α : Type u} [] (a : α) :
0 < a
theorem WithZero.zero_eq_bot {α : Type u} [] :
0 =
@[simp]
theorem WithZero.coe_lt_coe {α : Type u} [] {a : α} {b : α} :
a < b a < b
@[simp]
theorem WithZero.coe_le_coe {α : Type u} [] {a : α} {b : α} :
a b a b
instance WithZero.lattice {α : Type u} [] :
instance WithZero.linearOrder {α : Type u} [] :
instance WithZero.covariantClass_mul_le {α : Type u} [Mul α] [] [CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] :
CovariantClass () () (fun x x_1 => x * x_1) fun x x_1 => x x_1
theorem WithZero.le_max_iff {α : Type u} [] {a : α} {b : α} {c : α} :
a max b c a max b c
theorem WithZero.min_le_iff {α : Type u} [] {a : α} {b : α} {c : α} :
min a b c min a b c
theorem WithZero.covariantClass_add_le {α : Type u} [] [] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] (h : ∀ (a : α), 0 a) :
CovariantClass () () (fun x x_1 => x + x_1) fun x x_1 => x x_1
@[reducible]
def WithZero.orderedAddCommMonoid {α : Type u} (zero_le : ∀ (a : α), 0 a) :

If 0 is the least element in α, then WithZero α is an OrderedAddCommMonoid. See note [reducible non-instances].

Instances For