Documentation

Mathlib.Algebra.Order.Monoid.Basic

Ordered monoids #

This file develops some additional material on ordered monoids.

source
theorem Function.Injective.isOrderedMonoid {α : Type u} {β : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [One β] [Mul β] [Pow β ℕ] (f : β → α) (hf : Injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = f x * f y) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) :
have x := Injective.commMonoid f hf one mul npow; have x_1 := PartialOrder.lift f hf; IsOrderedMonoid β

Pullback an IsOrderedMonoid under an injective map.

source
theorem Function.Injective.isOrderedAddMonoid {α : Type u} {β : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [Zero β] [Add β] [SMul ℕ β] (f : β → α) (hf : Injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) (npow : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) :
have x := Injective.addCommMonoid f hf one mul npow; have x_1 := PartialOrder.lift f hf; IsOrderedAddMonoid β

Pullback an IsOrderedAddMonoid under an injective map.

source
theorem StrictMono.isOrderedMonoid {α : Type u} {β : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [CommMonoid β] [LinearOrder β] (f : β → α) (hf : StrictMono f) (mul : ∀ (x y : β), f (x * y) = f x * f y) :
IsOrderedMonoid β

Pullback an IsOrderedMonoid under a strictly monotone map.

source
theorem StrictMono.isOrderedAddMonoid {α : Type u} {β : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [AddCommMonoid β] [LinearOrder β] (f : β → α) (hf : StrictMono f) (mul : ∀ (x y : β), f (x + y) = f x + f y) :
IsOrderedAddMonoid β

Pullback an IsOrderedAddMonoid under a strictly monotone map.

source
theorem Function.Injective.isOrderedCancelMonoid {α : Type u} {β : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] [One β] [Mul β] [Pow β ℕ] (f : β → α) (hf : Injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = f x * f y) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) :
have x := Injective.commMonoid f hf one mul npow; have x_1 := PartialOrder.lift f hf; IsOrderedCancelMonoid β

Pullback an IsOrderedCancelMonoid under an injective map.

source
theorem Function.Injective.isOrderedCancelAddMonoid {α : Type u} {β : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [Zero β] [Add β] [SMul ℕ β] (f : β → α) (hf : Injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) (npow : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) :
have x := Injective.addCommMonoid f hf one mul npow; have x_1 := PartialOrder.lift f hf; IsOrderedCancelAddMonoid β

Pullback an IsOrderedCancelAddMonoid under an injective map.

source
theorem StrictMono.isOrderedCancelMonoid {α : Type u} {β : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] [CommMonoid β] [LinearOrder β] (f : β → α) (hf : StrictMono f) (mul : ∀ (x y : β), f (x * y) = f x * f y) :
IsOrderedCancelMonoid β

Pullback an IsOrderedCancelMonoid under a strictly monotone map.

source
theorem StrictMono.isOrderedAddCancelMonoid {α : Type u} {β : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [AddCommMonoid β] [LinearOrder β] (f : β → α) (hf : StrictMono f) (mul : ∀ (x y : β), f (x + y) = f x + f y) :
IsOrderedCancelAddMonoid β

Pullback an IsOrderedAddCancelMonoid under a strictly monotone map.

source
@[deprecated Function.Injective.isOrderedMonoid (since := "2025-04-10")]
theorem Function.Injective.orderedCommMonoid {α : Type u} {β : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [One β] [Mul β] [Pow β ℕ] (f : β → α) (hf : Injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = f x * f y) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) :
have x := Injective.commMonoid f hf one mul npow; have x_1 := PartialOrder.lift f hf; IsOrderedMonoid β

Alias of Function.Injective.isOrderedMonoid.

Pullback an IsOrderedMonoid under an injective map.

source
@[deprecated Function.Injective.isOrderedAddMonoid (since := "2025-04-10")]
theorem Function.Injective.orderedAddCommMonoid {α : Type u} {β : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [Zero β] [Add β] [SMul ℕ β] (f : β → α) (hf : Injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) (npow : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) :
have x := Injective.addCommMonoid f hf one mul npow; have x_1 := PartialOrder.lift f hf; IsOrderedAddMonoid β

Alias of Function.Injective.isOrderedAddMonoid.

Pullback an IsOrderedAddMonoid under an injective map.

source
@[deprecated Function.Injective.isOrderedCancelMonoid (since := "2025-04-10")]
theorem Function.Injective.orderedCancelCommMonoid {α : Type u} {β : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] [One β] [Mul β] [Pow β ℕ] (f : β → α) (hf : Injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = f x * f y) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) :
have x := Injective.commMonoid f hf one mul npow; have x_1 := PartialOrder.lift f hf; IsOrderedCancelMonoid β

Alias of Function.Injective.isOrderedCancelMonoid.

Pullback an IsOrderedCancelMonoid under an injective map.

source
@[deprecated Function.Injective.isOrderedCancelAddMonoid (since := "2025-04-10")]
theorem Function.Injective.orderedCancelAddCommMonoid {α : Type u} {β : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [Zero β] [Add β] [SMul ℕ β] (f : β → α) (hf : Injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) (npow : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) :
have x := Injective.addCommMonoid f hf one mul npow; have x_1 := PartialOrder.lift f hf; IsOrderedCancelAddMonoid β

Alias of Function.Injective.isOrderedCancelAddMonoid.

Pullback an IsOrderedCancelAddMonoid under an injective map.

source
@[deprecated Function.Injective.isOrderedMonoid (since := "2025-04-10")]
theorem Function.Injective.linearOrderedCommMonoid {α : Type u} {β : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [One β] [Mul β] [Pow β ℕ] (f : β → α) (hf : Injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = f x * f y) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) :
have x := Injective.commMonoid f hf one mul npow; have x_1 := PartialOrder.lift f hf; IsOrderedMonoid β

Alias of Function.Injective.isOrderedMonoid.

Pullback an IsOrderedMonoid under an injective map.

source
@[deprecated Function.Injective.isOrderedAddMonoid (since := "2025-04-10")]
theorem Function.Injective.linearOrderedAddCommMonoid {α : Type u} {β : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [Zero β] [Add β] [SMul ℕ β] (f : β → α) (hf : Injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) (npow : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) :
have x := Injective.addCommMonoid f hf one mul npow; have x_1 := PartialOrder.lift f hf; IsOrderedAddMonoid β

Alias of Function.Injective.isOrderedAddMonoid.

Pullback an IsOrderedAddMonoid under an injective map.

source
@[deprecated Function.Injective.isOrderedCancelMonoid (since := "2025-04-10")]
theorem Function.Injective.linearOrderedCancelCommMonoid {α : Type u} {β : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] [One β] [Mul β] [Pow β ℕ] (f : β → α) (hf : Injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = f x * f y) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) :
have x := Injective.commMonoid f hf one mul npow; have x_1 := PartialOrder.lift f hf; IsOrderedCancelMonoid β

Alias of Function.Injective.isOrderedCancelMonoid.

Pullback an IsOrderedCancelMonoid under an injective map.

source
@[deprecated Function.Injective.isOrderedCancelAddMonoid (since := "2025-04-10")]
theorem Function.Injective.linearOrderedCancelAddCommMonoid {α : Type u} {β : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [Zero β] [Add β] [SMul ℕ β] (f : β → α) (hf : Injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) (npow : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) :
have x := Injective.addCommMonoid f hf one mul npow; have x_1 := PartialOrder.lift f hf; IsOrderedCancelAddMonoid β

Alias of Function.Injective.isOrderedCancelAddMonoid.

Pullback an IsOrderedCancelAddMonoid under an injective map.

source
@[deprecated Function.Injective.isOrderedMonoid (since := "2025-04-10")]
theorem Function.Injective.orderedCommGroup {α : Type u} {β : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [One β] [Mul β] [Pow β ℕ] (f : β → α) (hf : Injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = f x * f y) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) :
have x := Injective.commMonoid f hf one mul npow; have x_1 := PartialOrder.lift f hf; IsOrderedMonoid β

Alias of Function.Injective.isOrderedMonoid.

Pullback an IsOrderedMonoid under an injective map.

source
@[deprecated Function.Injective.isOrderedAddMonoid (since := "2025-04-10")]
theorem Function.Injective.orderedAddCommGroup {α : Type u} {β : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [Zero β] [Add β] [SMul ℕ β] (f : β → α) (hf : Injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) (npow : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) :
have x := Injective.addCommMonoid f hf one mul npow; have x_1 := PartialOrder.lift f hf; IsOrderedAddMonoid β

Alias of Function.Injective.isOrderedAddMonoid.

Pullback an IsOrderedAddMonoid under an injective map.

source
@[deprecated Function.Injective.isOrderedMonoid (since := "2025-04-10")]
theorem Function.Injective.linearOrderedCommGroup {α : Type u} {β : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] [One β] [Mul β] [Pow β ℕ] (f : β → α) (hf : Injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = f x * f y) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) :
have x := Injective.commMonoid f hf one mul npow; have x_1 := PartialOrder.lift f hf; IsOrderedMonoid β

Alias of Function.Injective.isOrderedMonoid.

Pullback an IsOrderedMonoid under an injective map.

source
@[deprecated Function.Injective.isOrderedAddMonoid (since := "2025-04-10")]
theorem Function.Injective.linearOrderedAddCommGroup {α : Type u} {β : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] [Zero β] [Add β] [SMul ℕ β] (f : β → α) (hf : Injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) (npow : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) :
have x := Injective.addCommMonoid f hf one mul npow; have x_1 := PartialOrder.lift f hf; IsOrderedAddMonoid β

Alias of Function.Injective.isOrderedAddMonoid.

Pullback an IsOrderedAddMonoid under an injective map.

source
def OrderEmbedding.mulLeft {α : Type u_2} [Mul α] [LinearOrder α] [MulLeftStrictMono α] (m : α) :
α ↪o α

The order embedding sending b to a * b, for some fixed a. See also OrderIso.mulLeft when working in an ordered group.

Equations
    Instances For
      source
      def OrderEmbedding.addLeft {α : Type u_2} [Add α] [LinearOrder α] [AddLeftStrictMono α] (m : α) :
      α ↪o α

      The order embedding sending b to a + b, for some fixed a. See also OrderIso.addLeft when working in an additive ordered group.

      Equations
        Instances For
          source
          @[simp]
          theorem OrderEmbedding.addLeft_apply {α : Type u_2} [Add α] [LinearOrder α] [AddLeftStrictMono α] (m n : α) :
          (addLeft m) n = m + n
          source
          @[simp]
          theorem OrderEmbedding.mulLeft_apply {α : Type u_2} [Mul α] [LinearOrder α] [MulLeftStrictMono α] (m n : α) :
          (mulLeft m) n = m * n
          source
          def OrderEmbedding.mulRight {α : Type u_2} [Mul α] [LinearOrder α] [MulRightStrictMono α] (m : α) :
          α ↪o α

          The order embedding sending b to b * a, for some fixed a. See also OrderIso.mulRight when working in an ordered group.

          Equations
            Instances For
              source
              def OrderEmbedding.addRight {α : Type u_2} [Add α] [LinearOrder α] [AddRightStrictMono α] (m : α) :
              α ↪o α

              The order embedding sending b to b + a, for some fixed a. See also OrderIso.addRight when working in an additive ordered group.

              Equations
                Instances For
                  source
                  @[simp]
                  theorem OrderEmbedding.addRight_apply {α : Type u_2} [Add α] [LinearOrder α] [AddRightStrictMono α] (m n : α) :
                  (addRight m) n = n + m
                  source
                  @[simp]
                  theorem OrderEmbedding.mulRight_apply {α : Type u_2} [Mul α] [LinearOrder α] [MulRightStrictMono α] (m n : α) :
                  (mulRight m) n = n * m