Adjoining a zero element to an ordered monoid. #
class
LinearOrderedCommMonoidWithZero
(α : Type u_1)
extends
LinearOrderedCommMonoid
,
Zero
:
Type u_1
Zero is a left absorbing element for multiplication
Zero is a right absorbing element for multiplication
0 ≤ 1≤ 1
in any linearly ordered commutative monoid.zero_le_one : 0 ≤ 1
A linearly ordered commutative monoid with a zero element.
Instances
instance
LinearOrderedCommMonoidWithZero.toZeroLeOneClass
{α : Type u}
[inst : LinearOrderedCommMonoidWithZero α]
:
instance
CanonicallyOrderedAddMonoid.toZeroLeOneClass
{α : Type u}
[inst : CanonicallyOrderedAddMonoid α]
[inst : One α]
:
Equations
- WithZero.partialOrder = WithBot.partialOrder
Equations
- WithZero.linearOrder = WithBot.linearOrder
instance
WithZero.covariantClass_mul_le
{α : Type u}
[inst : Mul α]
[inst : Preorder α]
[inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
:
CovariantClass (WithZero α) (WithZero α) (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
Equations
- One or more equations did not get rendered due to their size.
theorem
WithZero.covariantClass_add_le
{α : Type u}
[inst : AddZeroClass α]
[inst : Preorder α]
[inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
(h : ∀ (a : α), 0 ≤ a)
:
CovariantClass (WithZero α) (WithZero α) (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
def
WithZero.orderedAddCommMonoid
{α : Type u}
[inst : OrderedAddCommMonoid α]
(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 : Preorder α]
[inst : ExistsAddOfLE α]
:
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 : CanonicallyLinearOrderedAddMonoid α]
:
Equations
- One or more equations did not get rendered due to their size.