# Documentation

Mathlib.Algebra.Order.Monoid.WithZero.Defs

# Adjoining a zero element to an ordered monoid. #

class LinearOrderedCommMonoidWithZero (α : Type u_1) extends , :
Type u_1
• Zero is a left absorbing element for multiplication

zero_mul : ∀ (a : α), 0 * a = 0
• Zero is a right absorbing element for multiplication

mul_zero : ∀ (a : α), a * 0 = 0
• 0 ≤ 1≤ 1 in any linearly ordered commutative monoid.

zero_le_one : 0 1

A linearly ordered commutative monoid with a zero element.

Instances
Equations
• LinearOrderedCommMonoidWithZero.toZeroLeOneClass = let src := inst; { zero_le_one := (_ : 0 1) }
instance CanonicallyOrderedAddMonoid.toZeroLeOneClass {α : Type u} [inst : ] [inst : One α] :
Equations
• CanonicallyOrderedAddMonoid.toZeroLeOneClass = { zero_le_one := (_ : 0 1) }
instance WithZero.preorder {α : Type u} [inst : ] :
Equations
• WithZero.preorder = WithBot.preorder
instance WithZero.partialOrder {α : Type u} [inst : ] :
Equations
• WithZero.partialOrder = WithBot.partialOrder
instance WithZero.orderBot {α : Type u} [inst : ] :
Equations
• WithZero.orderBot = WithBot.orderBot
theorem WithZero.zero_le {α : Type u} [inst : ] (a : ) :
0 a
theorem WithZero.zero_lt_coe {α : Type u} [inst : ] (a : α) :
0 < a
theorem WithZero.zero_eq_bot {α : Type u} [inst : ] :
0 =
@[simp]
theorem WithZero.coe_lt_coe {α : Type u} [inst : ] {a : α} {b : α} :
a < b a < b
@[simp]
theorem WithZero.coe_le_coe {α : Type u} [inst : ] {a : α} {b : α} :
a b a b
instance WithZero.lattice {α : Type u} [inst : ] :
Equations
• WithZero.lattice = WithBot.lattice
instance WithZero.linearOrder {α : Type u} [inst : ] :
Equations
• WithZero.linearOrder = WithBot.linearOrder
instance WithZero.covariantClass_mul_le {α : Type u} [inst : Mul α] [inst : ] [inst : 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
Equations
instance WithZero.orderedCommMonoid {α : Type u} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
theorem WithZero.covariantClass_add_le {α : Type u} [inst : ] [inst : ] [inst : 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
def WithZero.orderedAddCommMonoid {α : Type u} [inst : ] (zero_le : ∀ (a : α), 0 a) :

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

Equations
• One or more equations did not get rendered due to their size.
instance WithZero.existsAddOfLE {α : Type u} [inst : Add α] [inst : ] [inst : ] :
Equations
instance WithZero.canonicallyOrderedAddMonoid {α : Type u} [inst : ] :

Adding a new zero to a canonically ordered additive monoid produces another one.

Equations
• One or more equations did not get rendered due to their size.
instance WithZero.canonicallyLinearOrderedAddMonoid (α : Type u_1) [inst : ] :
Equations
• One or more equations did not get rendered due to their size.