# Units in ordered monoids #

instance AddUnits.instPreorder {α : Type u_1} [] [] :
Equations
instance Units.instPreorder {α : Type u_1} [] [] :
Equations
@[simp]
theorem AddUnits.val_le_val {α : Type u_1} [] [] {a : } {b : } :
a b a b
@[simp]
theorem Units.val_le_val {α : Type u_1} [] [] {a : αˣ} {b : αˣ} :
a b a b
@[simp]
theorem AddUnits.val_lt_val {α : Type u_1} [] [] {a : } {b : } :
a < b a < b
@[simp]
theorem Units.val_lt_val {α : Type u_1} [] [] {a : αˣ} {b : αˣ} :
a < b a < b
Equations
instance Units.instPartialOrderUnits {α : Type u_1} [] [] :
Equations
instance AddUnits.instLinearOrder {α : Type u_1} [] [] :
Equations
instance Units.instLinearOrder {α : Type u_1} [] [] :
Equations
theorem AddUnits.orderEmbeddingVal.proof_1 {α : Type u_1} [] [] :
∀ {a b : }, { toFun := AddUnits.val, inj' := } a { toFun := AddUnits.val, inj' := } b { toFun := AddUnits.val, inj' := } a { toFun := AddUnits.val, inj' := } b
def AddUnits.orderEmbeddingVal {α : Type u_1} [] [] :
↪o α

val : add_units α → α as an order embedding.

Equations
• AddUnits.orderEmbeddingVal = { toFun := AddUnits.val, inj' := , map_rel_iff' := }
Instances For
@[simp]
theorem AddUnits.orderEmbeddingVal_apply {α : Type u_1} [] [] :
@[simp]
theorem Units.orderEmbeddingVal_apply {α : Type u_1} [] [] :
Units.orderEmbeddingVal = Units.val
def Units.orderEmbeddingVal {α : Type u_1} [] [] :
αˣ ↪o α

val : αˣ → α as an order embedding.

Equations
• Units.orderEmbeddingVal = { toFun := Units.val, inj' := , map_rel_iff' := }
Instances For
@[simp]
theorem AddUnits.max_val {α : Type u_1} [] [] {a : } {b : } :
(max a b) = max a b
@[simp]
theorem Units.max_val {α : Type u_1} [] [] {a : αˣ} {b : αˣ} :
(max a b) = max a b
@[simp]
theorem AddUnits.min_val {α : Type u_1} [] [] {a : } {b : } :
(min a b) = min a b
@[simp]
theorem Units.min_val {α : Type u_1} [] [] {a : αˣ} {b : αˣ} :
(min a b) = min a b