Documentation

Mathlib.Algebra.Order.Monoid.Units

Units in ordered monoids #

source
instance Units.instPreorder {α : Type u_1} [Monoid α] [Preorder α] :
Preorder αˣ
Equations
    source
    instance AddUnits.instPreorder {α : Type u_1} [AddMonoid α] [Preorder α] :
    Preorder (AddUnits α)
    Equations
      source
      @[simp]
      theorem Units.val_le_val {α : Type u_1} [Monoid α] [Preorder α] {a b : αˣ} :
      ↑a ≤ ↑b ↔ a ≤ b
      source
      @[simp]
      theorem AddUnits.val_le_val {α : Type u_1} [AddMonoid α] [Preorder α] {a 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
      @[simp]
      theorem AddUnits.val_lt_val {α : Type u_1} [AddMonoid α] [Preorder α] {a b : AddUnits α} :
      ↑a < ↑b ↔ a < b
      source
      instance Units.instPartialOrderUnits {α : Type u_1} [Monoid α] [PartialOrder α] :
      PartialOrder αˣ
      Equations
        source
        instance AddUnits.instPartialOrderAddUnits {α : Type u_1} [AddMonoid α] [PartialOrder α] :
        PartialOrder (AddUnits α)
        Equations
          source
          instance Units.instLinearOrder {α : Type u_1} [Monoid α] [LinearOrder α] :
          LinearOrder αˣ
          Equations
            source
            instance AddUnits.instLinearOrder {α : Type u_1} [AddMonoid α] [LinearOrder α] :
            LinearOrder (AddUnits α)
            Equations
              source
              def Units.orderEmbeddingVal {α : Type u_1} [Monoid α] [LinearOrder α] :
              αˣ ↪o α

              val : αˣ → α as an order embedding.

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

                  val : add_units α → α as an order embedding.

                  Equations
                    Instances For
                      source
                      @[simp]
                      theorem AddUnits.orderEmbeddingVal_apply {α : Type u_1} [AddMonoid α] [LinearOrder α] :
                      ⇑orderEmbeddingVal = val
                      source
                      @[simp]
                      theorem Units.orderEmbeddingVal_apply {α : Type u_1} [Monoid α] [LinearOrder α] :
                      ⇑orderEmbeddingVal = val
                      source
                      @[simp]
                      theorem Units.max_val {α : Type u_1} [Monoid α] [LinearOrder α] {a b : αˣ} :
                      ↑(max a b) = max ↑a ↑b
                      source
                      @[simp]
                      theorem AddUnits.max_val {α : Type u_1} [AddMonoid α] [LinearOrder α] {a b : AddUnits α} :
                      ↑(max a b) = max ↑a ↑b
                      source
                      @[simp]
                      theorem Units.min_val {α : Type u_1} [Monoid α] [LinearOrder α] {a b : αˣ} :
                      ↑(min a b) = min ↑a ↑b
                      source
                      @[simp]
                      theorem AddUnits.min_val {α : Type u_1} [AddMonoid α] [LinearOrder α] {a b : AddUnits α} :
                      ↑(min a b) = min ↑a ↑b