Documentation

Mathlib.Algebra.Order.Monoid.WithZero.Defs

Adjoining a zero element to an ordered monoid. #

A linearly ordered commutative monoid with a zero element.

  • 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 : α), Monoid.npow 0 x = 1
  • npow_succ : ∀ (n : ) (x : α), Monoid.npow (n + 1) x = x * Monoid.npow n x
  • mul_comm : ∀ (a b : α), a * b = b * a
  • le : ααProp
  • lt : ααProp
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c : α), a bb ca c
  • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • mul_le_mul_left : ∀ (a b : α), a b∀ (c : α), c * a c * b
  • min : ααα
  • max : ααα
  • compare : ααOrdering
  • le_total : ∀ (a b : α), a b b a
  • decidableLE : DecidableRel fun (x x_1 : α) => x x_1
  • decidableEq : DecidableEq α
  • decidableLT : DecidableRel fun (x x_1 : α) => x < x_1
  • min_def : ∀ (a b : α), min a b = if a b then a else b
  • max_def : ∀ (a b : α), max a b = if a b then b else a
  • compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a b
  • zero : α
  • zero_mul : ∀ (a : α), 0 * a = 0

    Zero is a left absorbing element for multiplication

  • mul_zero : ∀ (a : α), a * 0 = 0

    Zero is a right absorbing element for multiplication

  • zero_le_one : 0 1

    0 ≤ 1 in any linearly ordered commutative monoid.

Instances
    instance WithZero.preorder {α : Type u} [Preorder α] :
    Equations
    • WithZero.preorder = WithBot.preorder
    Equations
    • WithZero.partialOrder = WithBot.partialOrder
    instance WithZero.orderBot {α : Type u} [Preorder α] :
    Equations
    • WithZero.orderBot = WithBot.orderBot
    theorem WithZero.zero_le {α : Type u} [Preorder α] (a : WithZero α) :
    0 a
    theorem WithZero.zero_lt_coe {α : Type u} [Preorder α] (a : α) :
    0 < a
    theorem WithZero.zero_eq_bot {α : Type u} [Preorder α] :
    0 =
    @[simp]
    theorem WithZero.coe_lt_coe {α : Type u} [Preorder α] {a : α} {b : α} :
    a < b a < b
    @[simp]
    theorem WithZero.coe_le_coe {α : Type u} [Preorder α] {a : α} {b : α} :
    a b a b
    instance WithZero.lattice {α : Type u} [Lattice α] :
    Equations
    • WithZero.lattice = WithBot.lattice
    Equations
    • WithZero.linearOrder = WithBot.linearOrder
    instance WithZero.covariantClass_mul_le {α : Type u} [Mul α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] :
    CovariantClass (WithZero α) (WithZero α) (fun (x x_1 : WithZero α) => x * x_1) fun (x x_1 : WithZero α) => x x_1
    Equations
    • =
    theorem WithZero.le_max_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} :
    a max b c a max b c
    theorem WithZero.min_le_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} :
    min a b c min a b c
    Equations
    • WithZero.orderedCommMonoid = let __src := CommMonoidWithZero.toCommMonoid; let __src_1 := WithZero.partialOrder; OrderedCommMonoid.mk
    theorem WithZero.covariantClass_add_le {α : Type u} [AddZeroClass α] [Preorder α] [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 : WithZero α) => x + x_1) fun (x x_1 : WithZero α) => x x_1
    @[reducible]
    def WithZero.orderedAddCommMonoid {α : Type u} [OrderedAddCommMonoid α] (zero_le : ∀ (a : α), 0 a) :

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

    Equations
    Instances For
      Equations
      • =

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

      Equations
      Equations
      • One or more equations did not get rendered due to their size.