Units in ordered monoids

instance Units.instPreorder {α : Type u_1} [Monoid α] [Preorder α] : Preorder αˣ

instance AddUnits.instPreorder {α : Type u_1} [AddMonoid α] [Preorder α] : Preorder (AddUnits α)

@[simp]

theorem Units.val_le_val {α : Type u_1} [Monoid α] [Preorder α] {a b : αˣ} : ↑a ≤ ↑b ↔ a ≤ b

@[simp]

theorem AddUnits.val_le_val {α : Type u_1} [AddMonoid α] [Preorder α] {a b : AddUnits α} : ↑a ≤ ↑b ↔ a ≤ b

@[simp]

theorem Units.val_lt_val {α : Type u_1} [Monoid α] [Preorder α] {a b : αˣ} : ↑a < ↑b ↔ a < b

@[simp]

theorem AddUnits.val_lt_val {α : Type u_1} [AddMonoid α] [Preorder α] {a b : AddUnits α} : ↑a < ↑b ↔ a < b

instance Units.instPartialOrderUnits {α : Type u_1} [Monoid α] [PartialOrder α] : PartialOrder αˣ

instance AddUnits.instPartialOrderAddUnits {α : Type u_1} [AddMonoid α] [PartialOrder α] : PartialOrder (AddUnits α)

instance Units.instMaxOfLinearOrder {α : Type u_1} [Monoid α] [LinearOrder α] : Max αˣ

instance AddUnits.instMaxOfLinearOrder {α : Type u_1} [AddMonoid α] [LinearOrder α] : Max (AddUnits α)

instance Units.instMinOfLinearOrder {α : Type u_1} [Monoid α] [LinearOrder α] : Min αˣ

instance AddUnits.instMinOfLinearOrder {α : Type u_1} [AddMonoid α] [LinearOrder α] : Min (AddUnits α)

@[simp]

theorem Units.max_val {α : Type u_1} [Monoid α] [LinearOrder α] (a b : αˣ) : ↑(max a b) = max ↑a ↑b

@[simp]

theorem AddUnits.max_val {α : Type u_1} [AddMonoid α] [LinearOrder α] (a b : AddUnits α) : ↑(max a b) = max ↑a ↑b

@[simp]

theorem Units.min_val {α : Type u_1} [Monoid α] [LinearOrder α] (a b : αˣ) : ↑(min a b) = min ↑a ↑b

@[simp]

theorem AddUnits.min_val {α : Type u_1} [AddMonoid α] [LinearOrder α] (a b : AddUnits α) : ↑(min a b) = min ↑a ↑b

instance Units.instOrd {α : Type u_1} [Monoid α] [Ord α] : Ord αˣ

instance AddUnits.instOrd {α : Type u_1} [AddMonoid α] [Ord α] : Ord (AddUnits α)

theorem Units.compare_val {α : Type u_1} [Monoid α] [Ord α] (a b : αˣ) : compare ↑a ↑b = compare a b

theorem AddUnits.compare_val {α : Type u_1} [AddMonoid α] [Ord α] (a b : AddUnits α) : compare ↑a ↑b = compare a b

instance Units.instLinearOrder {α : Type u_1} [Monoid α] [LinearOrder α] : LinearOrder αˣ

instance AddUnits.instLinearOrder {α : Type u_1} [AddMonoid α] [LinearOrder α] : LinearOrder (AddUnits α)

def Units.orderEmbeddingVal {α : Type u_1} [Monoid α] [LinearOrder α] : αˣ ↪o α

val : αˣ → α as an order embedding.

def AddUnits.orderEmbeddingVal {α : Type u_1} [AddMonoid α] [LinearOrder α] : AddUnits α ↪o α

val : add_units α → α as an order embedding.

@[simp]

theorem AddUnits.orderEmbeddingVal_apply {α : Type u_1} [AddMonoid α] [LinearOrder α] : ⇑orderEmbeddingVal = val

@[simp]

theorem Units.orderEmbeddingVal_apply {α : Type u_1} [Monoid α] [LinearOrder α] : ⇑orderEmbeddingVal = val