Adjoining a zero element to an ordered monoid.

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

• 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
• 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
• 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
• mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * 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.

A linearly ordered commutative monoid with a zero element.

instance LinearOrderedCommMonoidWithZero.toZeroLeOneClass {α : Type u} [LinearOrderedCommMonoidWithZero α] : ZeroLEOneClass α

Equations

• @LinearOrderedCommMonoidWithZero.toZeroLeOneClass = @LinearOrderedCommMonoidWithZero.toZeroLeOneClass.proof_1

instance CanonicallyOrderedAddMonoid.toZeroLeOneClass {α : Type u} [CanonicallyOrderedAddMonoid α] [One α] : ZeroLEOneClass α

Equations

• @CanonicallyOrderedAddMonoid.toZeroLeOneClass = @CanonicallyOrderedAddMonoid.toZeroLeOneClass.proof_1

instance WithZero.preorder {α : Type u} [Preorder α] : Preorder (WithZero α)

Equations

• WithZero.preorder = WithBot.preorder

instance WithZero.partialOrder {α : Type u} [PartialOrder α] : PartialOrder (WithZero α)

Equations

• WithZero.partialOrder = WithBot.partialOrder

instance WithZero.orderBot {α : Type u} [Preorder α] : OrderBot (WithZero α)

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 α] : Lattice (WithZero α)

Equations

• WithZero.lattice = WithBot.lattice

instance WithZero.linearOrder {α : Type u} [LinearOrder α] : LinearOrder (WithZero α)

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 => x * x_1) fun x x_1 => x ≤ x_1

Equations

• @WithZero.covariantClass_mul_le = @WithZero.covariantClass_mul_le.proof_1

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

instance WithZero.orderedCommMonoid {α : Type u} [OrderedCommMonoid α] : OrderedCommMonoid (WithZero α)

Equations

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

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 => x + x_1) fun x x_1 => x ≤ x_1

@[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

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

instance WithZero.existsAddOfLE {α : Type u} [Add α] [Preorder α] [ExistsAddOfLE α] : ExistsAddOfLE (WithZero α)

Equations

• @WithZero.existsAddOfLE = @WithZero.existsAddOfLE.proof_1

instance WithZero.canonicallyOrderedAddMonoid {α : Type u} [CanonicallyOrderedAddMonoid α] : CanonicallyOrderedAddMonoid (WithZero α)

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) [CanonicallyLinearOrderedAddMonoid α] : CanonicallyLinearOrderedAddMonoid (WithZero α)

Equations

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