Ordered structures on localizations of commutative monoids

@[implicit_reducible]

instance Localization.le {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} : LE (Localization s)

@[implicit_reducible]

instance AddLocalization.le {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} : LE (AddLocalization s)

@[implicit_reducible]

instance Localization.lt {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} : LT (Localization s)

@[implicit_reducible]

instance AddLocalization.lt {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} : LT (AddLocalization s)

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₁

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₁

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₁

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₁

@[implicit_reducible]

instance Localization.partialOrder {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} : PartialOrder (Localization s)

@[implicit_reducible]

instance AddLocalization.partialOrder {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} : PartialOrder (AddLocalization s)

instance Localization.isOrderedCancelMonoid {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} : IsOrderedCancelMonoid (Localization s)

instance AddLocalization.isOrderedAddCancelMonoid {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} : IsOrderedCancelAddMonoid (AddLocalization s)

@[implicit_reducible]

instance Localization.decidableLE {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} [DecidableLE α] : DecidableLE (Localization s)

@[implicit_reducible]

instance AddLocalization.decidableLE {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} [DecidableLE α] : DecidableLE (AddLocalization s)

@[implicit_reducible]

instance Localization.decidableLT {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} [DecidableLT α] : DecidableLT (Localization s)

@[implicit_reducible]

instance AddLocalization.decidableLT {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} [DecidableLT α] : DecidableLT (AddLocalization s)

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.

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.

@[simp]

theorem Localization.mkOrderEmbedding_apply {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} (b : ↥s) (a : α) : (mkOrderEmbedding b) a = mk a b

@[simp]

theorem AddLocalization.mkOrderEmbedding_apply {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} (b : ↥s) (a : α) : (mkOrderEmbedding b) a = mk a b

@[implicit_reducible]

instance Localization.instLinearOrderOfIsOrderedCancelMonoid {α : Type u_1} [CommMonoid α] [LinearOrder α] [IsOrderedCancelMonoid α] {s : Submonoid α} : LinearOrder (Localization s)

@[implicit_reducible]

instance AddLocalization.instLinearAddOrderOfIsOrderedAddCancelMonoid {α : Type u_1} [AddCommMonoid α] [LinearOrder α] [IsOrderedCancelAddMonoid α] {s : AddSubmonoid α} : LinearOrder (AddLocalization s)