Documentation

Mathlib.Algebra.Order.Monoid.WithZero.Defs

Adjoining a zero element to an ordered monoid. #

source
class LinearOrderedCommMonoidWithZero (α : Type u_1) extends LinearOrderedCommMonoid , Zero :
Type u_1

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 ≤ b → b ≤ c → a ≤ c
  • lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = 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
    source
    instance LinearOrderedCommMonoidWithZero.toZeroLeOneClass {α : Type u} [LinearOrderedCommMonoidWithZero α] :
    ZeroLEOneClass α
    Equations
    • ⋯ = ⋯
    source
    instance canonicallyOrderedAddCommMonoid.toZeroLeOneClass {α : Type u} [CanonicallyOrderedAddCommMonoid α] [One α] :
    ZeroLEOneClass α
    Equations
    • ⋯ = ⋯
    source
    instance WithZero.preorder {α : Type u} [Preorder α] :
    Preorder (WithZero α)
    Equations
    • WithZero.preorder = WithBot.preorder
    source
    instance WithZero.partialOrder {α : Type u} [PartialOrder α] :
    PartialOrder (WithZero α)
    Equations
    • WithZero.partialOrder = WithBot.partialOrder
    source
    instance WithZero.orderBot {α : Type u} [Preorder α] :
    OrderBot (WithZero α)
    Equations
    • WithZero.orderBot = WithBot.orderBot
    source
    theorem WithZero.zero_le {α : Type u} [Preorder α] (a : WithZero α) :
    0 ≤ a
    source
    theorem WithZero.zero_lt_coe {α : Type u} [Preorder α] (a : α) :
    0 < ↑a
    source
    theorem WithZero.zero_eq_bot {α : Type u} [Preorder α] :
    0 = ⊥
    source
    @[simp]
    theorem WithZero.coe_lt_coe {α : Type u} [Preorder α] {a : α} {b : α} :
    ↑a < ↑b ↔ a < b
    source
    @[simp]
    theorem WithZero.coe_le_coe {α : Type u} [Preorder α] {a : α} {b : α} :
    ↑a ≤ ↑b ↔ a ≤ b
    source
    instance WithZero.lattice {α : Type u} [Lattice α] :
    Lattice (WithZero α)
    Equations
    • WithZero.lattice = WithBot.lattice
    source
    instance WithZero.linearOrder {α : Type u} [LinearOrder α] :
    LinearOrder (WithZero α)
    Equations
    • WithZero.linearOrder = WithBot.linearOrder
    source
    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
    • ⋯ = ⋯
    source
    theorem WithZero.le_max_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} :
    ↑a ≤ max ↑b ↑c ↔ a ≤ max b c
    source
    theorem WithZero.min_le_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} :
    min ↑a ↑b ≤ ↑c ↔ min a b ≤ c
    source
    instance WithZero.orderedCommMonoid {α : Type u} [OrderedCommMonoid α] :
    OrderedCommMonoid (WithZero α)
    Equations
    • WithZero.orderedCommMonoid = let __src := CommMonoidWithZero.toCommMonoid; let __src_1 := WithZero.partialOrder; OrderedCommMonoid.mk ⋯
    source
    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
    source
    @[reducible]
    def WithZero.orderedAddCommMonoid {α : Type u} [OrderedAddCommMonoid α] (zero_le : ∀ (a : α), 0 ≤ a) :
    OrderedAddCommMonoid (WithZero α)

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

    Equations
    Instances For
      source
      instance WithZero.existsAddOfLE {α : Type u} [Add α] [Preorder α] [ExistsAddOfLE α] :
      ExistsAddOfLE (WithZero α)
      Equations
      • ⋯ = ⋯
      source
      instance WithZero.canonicallyOrderedAddCommMonoid {α : Type u} [CanonicallyOrderedAddCommMonoid α] :
      CanonicallyOrderedAddCommMonoid (WithZero α)

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

      Equations
      source
      instance WithZero.canonicallyLinearOrderedAddCommMonoid (α : Type u_1) [CanonicallyLinearOrderedAddCommMonoid α] :
      CanonicallyLinearOrderedAddCommMonoid (WithZero α)
      Equations
      • One or more equations did not get rendered due to their size.