Documentation

Mathlib.GroupTheory.MonoidLocalization.Order

Ordered structures on localizations of commutative monoids #

source
instance Localization.le {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} :
LE (Localization s)
Equations
    source
    instance AddLocalization.le {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} :
    LE (AddLocalization s)
    Equations
      source
      instance Localization.lt {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} :
      LT (Localization s)
      Equations
        source
        instance AddLocalization.lt {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} :
        LT (AddLocalization s)
        Equations
          source
          theorem Localization.mk_le_mk {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s} :
          mk a₁ a₂ ≤ mk b₁ b₂ ↔ ↑b₂ * a₁ ≤ ↑a₂ * b₁
          source
          theorem AddLocalization.mk_le_mk {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s} :
          mk a₁ a₂ ≤ mk b₁ b₂ ↔ ↑b₂ + a₁ ≤ ↑a₂ + b₁
          source
          theorem Localization.mk_lt_mk {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s} :
          mk a₁ a₂ < mk b₁ b₂ ↔ ↑b₂ * a₁ < ↑a₂ * b₁
          source
          theorem AddLocalization.mk_lt_mk {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s} :
          mk a₁ a₂ < mk b₁ b₂ ↔ ↑b₂ + a₁ < ↑a₂ + b₁
          source
          instance Localization.partialOrder {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} :
          PartialOrder (Localization s)
          Equations
            source
            instance AddLocalization.partialOrder {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} :
            PartialOrder (AddLocalization s)
            Equations
              source
              instance Localization.isOrderedCancelMonoid {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} :
              IsOrderedCancelMonoid (Localization s)
              source
              instance AddLocalization.isOrderedAddCancelMonoid {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} :
              IsOrderedCancelAddMonoid (AddLocalization s)
              source
              instance Localization.decidableLE {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} [DecidableLE α] :
              DecidableLE (Localization s)
              Equations
                source
                instance AddLocalization.decidableLE {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} [DecidableLE α] :
                DecidableLE (AddLocalization s)
                Equations
                  source
                  instance Localization.decidableLT {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} [DecidableLT α] :
                  DecidableLT (Localization s)
                  Equations
                    source
                    instance AddLocalization.decidableLT {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} [DecidableLT α] :
                    DecidableLT (AddLocalization s)
                    Equations
                      source
                      def Localization.mkOrderEmbedding {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} (b : ↥s) :
                      α ↪o Localization s

                      An ordered cancellative monoid injects into its localization by sending a to a / b.

                      Equations
                        Instances For
                          source
                          def AddLocalization.mkOrderEmbedding {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} (b : ↥s) :
                          α ↪o AddLocalization s

                          An ordered cancellative monoid injects into its localization by sending a to a - b.

                          Equations
                            Instances For
                              source
                              @[simp]
                              theorem AddLocalization.mkOrderEmbedding_apply {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} (b : ↥s) (a : α) :
                              (mkOrderEmbedding b) a = mk a b
                              source
                              @[simp]
                              theorem Localization.mkOrderEmbedding_apply {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} (b : ↥s) (a : α) :
                              (mkOrderEmbedding b) a = mk a b
                              source
                              instance Localization.instLinearOrderOfIsOrderedCancelMonoid {α : Type u_1} [CommMonoid α] [LinearOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} :
                              LinearOrder (Localization s)
                              Equations
                                source
                                instance AddLocalization.instLinearAddOrderOfIsOrderedAddCancelMonoid {α : Type u_1} [AddCommMonoid α] [LinearOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} :
                                LinearOrder (AddLocalization s)
                                Equations