Documentation

Mathlib.Algebra.Order.Monoid.Units

Units in ordered monoids #

source
🔸 coverage
@[implicit_reducible]
instance Units.instPreorder {α : Type u_1} [Monoid α] [Preorder α] :
Preorder αˣ
source
🔸 coverage
@[implicit_reducible]
instance AddUnits.instPreorder {α : Type u_1} [AddMonoid α] [Preorder α] :
Preorder (AddUnits α)
source
📐 coverage
@[simp]
theorem Units.val_le_val {α : Type u_1} [Monoid α] [Preorder α] {a b : αˣ} :
↑a ≤ ↑b ↔ a ≤ b
source
📐 coverage
@[simp]
theorem AddUnits.val_le_val {α : Type u_1} [AddMonoid α] [Preorder α] {a b : AddUnits α} :
↑a ≤ ↑b ↔ a ≤ b
source
📐 coverage
@[simp]
theorem Units.val_lt_val {α : Type u_1} [Monoid α] [Preorder α] {a b : αˣ} :
↑a < ↑b ↔ a < b
source
📐 coverage
@[simp]
theorem AddUnits.val_lt_val {α : Type u_1} [AddMonoid α] [Preorder α] {a b : AddUnits α} :
↑a < ↑b ↔ a < b
source
🔸 coverage
@[implicit_reducible]
instance Units.instPartialOrderUnits {α : Type u_1} [Monoid α] [PartialOrder α] :
PartialOrder αˣ
source
🔸 coverage
@[implicit_reducible]
instance AddUnits.instPartialOrderAddUnits {α : Type u_1} [AddMonoid α] [PartialOrder α] :
PartialOrder (AddUnits α)
source
🔸 coverage
@[implicit_reducible]
instance Units.instMaxOfLinearOrder {α : Type u_1} [Monoid α] [LinearOrder α] :
Max αˣ
source
🔸 coverage
@[implicit_reducible]
instance AddUnits.instMaxOfLinearOrder {α : Type u_1} [AddMonoid α] [LinearOrder α] :
Max (AddUnits α)
source
🔸 coverage
@[implicit_reducible]
instance Units.instMinOfLinearOrder {α : Type u_1} [Monoid α] [LinearOrder α] :
Min αˣ
source
🔸 coverage
@[implicit_reducible]
instance AddUnits.instMinOfLinearOrder {α : Type u_1} [AddMonoid α] [LinearOrder α] :
Min (AddUnits α)
source
📐 coverage
@[simp]
theorem Units.max_val {α : Type u_1} [Monoid α] [LinearOrder α] (a b : αˣ) :
↑(max a b) = max ↑a ↑b
source
📐 coverage
@[simp]
theorem AddUnits.max_val {α : Type u_1} [AddMonoid α] [LinearOrder α] (a b : AddUnits α) :
↑(max a b) = max ↑a ↑b
source
📐 coverage
@[simp]
theorem Units.min_val {α : Type u_1} [Monoid α] [LinearOrder α] (a b : αˣ) :
↑(min a b) = min ↑a ↑b
source
📐 coverage
@[simp]
theorem AddUnits.min_val {α : Type u_1} [AddMonoid α] [LinearOrder α] (a b : AddUnits α) :
↑(min a b) = min ↑a ↑b
source
🔸 coverage
@[implicit_reducible]
instance Units.instOrd {α : Type u_1} [Monoid α] [Ord α] :
Ord αˣ
source
🔸 coverage
@[implicit_reducible]
instance AddUnits.instOrd {α : Type u_1} [AddMonoid α] [Ord α] :
Ord (AddUnits α)
source
📐 coverage
theorem Units.compare_val {α : Type u_1} [Monoid α] [Ord α] (a b : αˣ) :
compare ↑a ↑b = compare a b
source
📐 coverage
theorem AddUnits.compare_val {α : Type u_1} [AddMonoid α] [Ord α] (a b : AddUnits α) :
compare ↑a ↑b = compare a b
source
🔸 coverage
@[implicit_reducible]
instance Units.instLinearOrder {α : Type u_1} [Monoid α] [LinearOrder α] :
LinearOrder αˣ
source
🔸 coverage
@[implicit_reducible]
instance AddUnits.instLinearOrder {α : Type u_1} [AddMonoid α] [LinearOrder α] :
LinearOrder (AddUnits α)
source
🔸 coverage
def Units.orderEmbeddingVal {α : Type u_1} [Monoid α] [LinearOrder α] :
αˣ ↪o α

val : αˣ → α as an order embedding.

Instances For
    source
    🔸 coverage
    def AddUnits.orderEmbeddingVal {α : Type u_1} [AddMonoid α] [LinearOrder α] :
    AddUnits α ↪o α

    val : add_units α → α as an order embedding.

    Instances For
      source
      📐 coverage
      @[simp]
      theorem AddUnits.orderEmbeddingVal_apply {α : Type u_1} [AddMonoid α] [LinearOrder α] :
      ⇑orderEmbeddingVal = val
      source
      📐 coverage
      @[simp]
      theorem Units.orderEmbeddingVal_apply {α : Type u_1} [Monoid α] [LinearOrder α] :
      ⇑orderEmbeddingVal = val