Documentation

Mathlib.Algebra.Order.Monoid.WithZero.Defs

Adjoining a zero element to an ordered monoid. #

  • 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) }
    Equations
    • CanonicallyOrderedAddMonoid.toZeroLeOneClass = { zero_le_one := (_ : 0 1) }
    instance WithZero.preorder {α : Type u} [inst : Preorder α] :
    Equations
    • WithZero.preorder = WithBot.preorder
    instance WithZero.partialOrder {α : Type u} [inst : PartialOrder α] :
    Equations
    • WithZero.partialOrder = WithBot.partialOrder
    instance WithZero.orderBot {α : Type u} [inst : Preorder α] :
    Equations
    • WithZero.orderBot = WithBot.orderBot
    theorem WithZero.zero_le {α : Type u} [inst : Preorder α] (a : WithZero α) :
    0 a
    theorem WithZero.zero_lt_coe {α : Type u} [inst : Preorder α] (a : α) :
    0 < a
    theorem WithZero.zero_eq_bot {α : Type u} [inst : Preorder α] :
    0 =
    @[simp]
    theorem WithZero.coe_lt_coe {α : Type u} [inst : Preorder α] {a : α} {b : α} :
    a < b a < b
    @[simp]
    theorem WithZero.coe_le_coe {α : Type u} [inst : Preorder α] {a : α} {b : α} :
    a b a b
    instance WithZero.lattice {α : Type u} [inst : Lattice α] :
    Equations
    • WithZero.lattice = WithBot.lattice
    instance WithZero.linearOrder {α : Type u} [inst : LinearOrder α] :
    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
    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.

    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.
    Equations
    • One or more equations did not get rendered due to their size.