HepLean Documentation

Mathlib.Algebra.Order.Monoid.Units

Units in ordered monoids #

source
instance AddUnits.instPreorder {α : Type u_1} [AddMonoid α] [Preorder α] :
Preorder (AddUnits α)
Equations
source
instance Units.instPreorder {α : Type u_1} [Monoid α] [Preorder α] :
Preorder αˣ
Equations
source
@[simp]
theorem AddUnits.val_le_val {α : Type u_1} [AddMonoid α] [Preorder α] {a : AddUnits α} {b : AddUnits α} :
↑a ≤ ↑b ↔ a ≤ b
source
@[simp]
theorem Units.val_le_val {α : Type u_1} [Monoid α] [Preorder α] {a : αˣ} {b : αˣ} :
↑a ≤ ↑b ↔ a ≤ b
source
@[simp]
theorem AddUnits.val_lt_val {α : Type u_1} [AddMonoid α] [Preorder α] {a : AddUnits α} {b : AddUnits α} :
↑a < ↑b ↔ a < b
source
@[simp]
theorem Units.val_lt_val {α : Type u_1} [Monoid α] [Preorder α] {a : αˣ} {b : αˣ} :
↑a < ↑b ↔ a < b
source
instance AddUnits.instPartialOrderAddUnits {α : Type u_1} [AddMonoid α] [PartialOrder α] :
PartialOrder (AddUnits α)
Equations
source
instance Units.instPartialOrderUnits {α : Type u_1} [Monoid α] [PartialOrder α] :
PartialOrder αˣ
Equations
source
instance AddUnits.instLinearOrder {α : Type u_1} [AddMonoid α] [LinearOrder α] :
LinearOrder (AddUnits α)
Equations
source
instance Units.instLinearOrder {α : Type u_1} [Monoid α] [LinearOrder α] :
LinearOrder αˣ
Equations
source
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' := ⋯ }
Instances For
    source
    theorem AddUnits.orderEmbeddingVal.proof_1 {α : Type u_1} [AddMonoid α] [LinearOrder α] :
    ∀ {a b : AddUnits α}, { toFun := AddUnits.val, inj' := ⋯ } a ≤ { toFun := AddUnits.val, inj' := ⋯ } b ↔ { toFun := AddUnits.val, inj' := ⋯ } a ≤ { toFun := AddUnits.val, inj' := ⋯ } b
    source
    @[simp]
    theorem AddUnits.orderEmbeddingVal_apply {α : Type u_1} [AddMonoid α] [LinearOrder α] :
    ⇑AddUnits.orderEmbeddingVal = AddUnits.val
    source
    @[simp]
    theorem Units.orderEmbeddingVal_apply {α : Type u_1} [Monoid α] [LinearOrder α] :
    ⇑Units.orderEmbeddingVal = Units.val
    source
    def Units.orderEmbeddingVal {α : Type u_1} [Monoid α] [LinearOrder α] :
    αˣ ↪o α

    val : αˣ → α as an order embedding.

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