Units in ordered monoids

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

Equations

• Units.instPreorder = Preorder.lift Units.val

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

Equations

• AddUnits.instPreorder = Preorder.lift AddUnits.val

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

Equations

• Units.instPartialOrderUnits = PartialOrder.lift Units.val ⋯

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

Equations

• AddUnits.instPartialOrderAddUnits = PartialOrder.lift AddUnits.val ⋯

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

Equations

• Units.instMaxOfLinearOrder = { max := fun (a b : αˣ) => if a ≤ b then b else a }

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

Equations

• AddUnits.instMaxOfLinearOrder = { max := fun (a b : AddUnits α) => if a ≤ b then b else a }

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

Equations

• Units.instMinOfLinearOrder = { min := fun (a b : αˣ) => if a ≤ b then a else b }

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

Equations

• AddUnits.instMinOfLinearOrder = { min := fun (a b : AddUnits α) => if a ≤ b then a else b }

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

Equations

• Units.instOrd = { compare := fun (a b : αˣ) => compare ↑a ↑b }

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

Equations

• AddUnits.instOrd = { compare := fun (a b : AddUnits α) => compare ↑a ↑b }

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 αˣ

Equations

• Units.instLinearOrder = Function.Injective.linearOrder Units.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• AddUnits.instLinearOrder = Function.Injective.linearOrder AddUnits.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

val : αˣ → α as an order embedding.

Equations

• Units.orderEmbeddingVal = { toFun := Units.val, inj' := ⋯, map_rel_iff' := ⋯ }

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

val : add_units α → α as an order embedding.

Equations

• AddUnits.orderEmbeddingVal = { toFun := AddUnits.val, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

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

@[simp]

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