mathlib3 documentation

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.

@[class]
structure linear_ordered_comm_monoid_with_zero (α : Type u_1) :
Type u_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
@[protected, instance]
def with_zero.preorder {α : Type u} [preorder α] :
Equations
@[protected, instance]
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
@[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]