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.instMaxOfLinearOrder {α : Type u_1} [Monoid α] [LinearOrder α] :
          Max αˣ
          Equations
            source
            instance AddUnits.instMaxOfLinearOrder {α : Type u_1} [AddMonoid α] [LinearOrder α] :
            Max (AddUnits α)
            Equations
              source
              instance Units.instMinOfLinearOrder {α : Type u_1} [Monoid α] [LinearOrder α] :
              Min αˣ
              Equations
                source
                instance AddUnits.instMinOfLinearOrder {α : Type u_1} [AddMonoid α] [LinearOrder α] :
                Min (AddUnits α)
                Equations
                  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
                  source
                  instance Units.instOrd {α : Type u_1} [Monoid α] [Ord α] :
                  Ord αˣ
                  Equations
                    source
                    instance AddUnits.instOrd {α : Type u_1} [AddMonoid α] [Ord α] :
                    Ord (AddUnits α)
                    Equations
                      source
                      theorem Units.compare_val {α : Type u_1} [Monoid α] [Ord α] (a b : αˣ) :
                      compare ↑a ↑b = compare a b
                      source
                      theorem AddUnits.compare_val {α : Type u_1} [AddMonoid α] [Ord α] (a b : AddUnits α) :
                      compare ↑a ↑b = compare a b
                      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 Units.orderEmbeddingVal_apply {α : Type u_1} [Monoid α] [LinearOrder α] :
                                  ⇑orderEmbeddingVal = val
                                  source
                                  @[simp]
                                  theorem AddUnits.orderEmbeddingVal_apply {α : Type u_1} [AddMonoid α] [LinearOrder α] :
                                  ⇑orderEmbeddingVal = val