# mathlib3documentation

algebra.order.monoid.with_zero.defs

# Adjoining a zero element to an ordered monoid. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[instance]
@[class]
structure linear_ordered_comm_monoid_with_zero (α : Type u_1) :
Type u_1
• 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_eq :
• decidable_lt :
• max : α α α
• max_def : . "reflexivity"
• min : α α α
• min_def : . "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 : α), . "try_refl_tac"
• npow_succ' : ( (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
Instances of other typeclasses for linear_ordered_comm_monoid_with_zero
• linear_ordered_comm_monoid_with_zero.has_sizeof_inst
@[instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def with_zero.preorder {α : Type u} [preorder α] :
Equations
@[protected, instance]
def with_zero.partial_order {α : Type u}  :
Equations
@[protected, instance]
def with_zero.order_bot {α : Type u} [preorder α] :
Equations
theorem with_zero.zero_le {α : Type u} [preorder α] (a : with_zero α) :
0 a
theorem with_zero.zero_lt_coe {α : Type u} [preorder α] (a : α) :
0 < a
theorem with_zero.zero_eq_bot {α : Type u} [preorder α] :
0 =
@[simp, norm_cast]
theorem with_zero.coe_lt_coe {α : Type u} [preorder α] {a b : α} :
a < b a < b
@[simp, norm_cast]
theorem with_zero.coe_le_coe {α : Type u} [preorder α] {a b : α} :
a b a b
@[protected, instance]
def with_zero.lattice {α : Type u} [lattice α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
@[simp]
theorem with_zero.le_max_iff {α : Type u} [linear_order α] {a b c : α} :
@[simp]
theorem with_zero.min_le_iff {α : Type u} [linear_order α] {a b c : α} :
@[protected, instance]
Equations
@[protected]
theorem with_zero.covariant_class_add_le {α : Type u} [preorder α] (h : (a : α), 0 a) :
@[protected, reducible]
def with_zero.ordered_add_comm_monoid {α : Type u} (zero_le : (a : α), 0 a) :

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

Equations
@[protected, instance]
def with_zero.has_exists_add_of_le {α : Type u_1} [has_add α] [preorder α]  :
@[protected, instance]

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

Equations
@[protected, instance]
Equations