Documentation

Mathlib.GroupTheory.Submonoid.Order

Ordered instances on submonoids #

theorem AddSubmonoidClass.toOrderedAddCommMonoid.proof_2 {M : Type u_1} {S : Type u_2} [SetLike S M] (s : S) :
Function.Injective fun (a : s) => a
theorem AddSubmonoidClass.toOrderedAddCommMonoid.proof_4 {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedAddCommMonoid M] [AddSubmonoidClass S M] (s : S) :
∀ (x x_1 : s), (x + x_1) = (x + x_1)
theorem AddSubmonoidClass.toOrderedAddCommMonoid.proof_5 {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedAddCommMonoid M] [AddSubmonoidClass S M] (s : S) :
∀ (x : s) (x_1 : ), (x_1 x) = (x_1 x)
theorem AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_7 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedAddCommMonoid M] (s : S) :
∀ (x x_1 : s), (x x_1) = (x x_1)
theorem AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_6 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedAddCommMonoid M] (s : S) :
∀ (x x_1 : s), (x x_1) = (x x_1)
theorem AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_5 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedAddCommMonoid M] [AddSubmonoidClass S M] (s : S) :
∀ (x : s) (x_1 : ), (x_1 x) = (x_1 x)
theorem AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_4 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedAddCommMonoid M] [AddSubmonoidClass S M] (s : S) :
∀ (x x_1 : s), (x + x_1) = (x + x_1)
theorem AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_2 {M : Type u_1} {S : Type u_2} [SetLike S M] (s : S) :
Function.Injective fun (a : s) => a
theorem AddSubmonoidClass.toOrderedCancelAddCommMonoid.proof_5 {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedCancelAddCommMonoid M] [AddSubmonoidClass S M] (s : S) :
∀ (x : s) (x_1 : ), (x_1 x) = (x_1 x)
theorem AddSubmonoidClass.toOrderedCancelAddCommMonoid.proof_4 {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedCancelAddCommMonoid M] [AddSubmonoidClass S M] (s : S) :
∀ (x x_1 : s), (x + x_1) = (x + x_1)
theorem AddSubmonoidClass.toOrderedCancelAddCommMonoid.proof_2 {M : Type u_1} {S : Type u_2} [SetLike S M] (s : S) :
Function.Injective fun (a : s) => a
theorem AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_4 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedCancelAddCommMonoid M] [AddSubmonoidClass S M] (s : S) :
∀ (x x_1 : s), (x + x_1) = (x + x_1)
theorem AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_2 {M : Type u_1} {S : Type u_2} [SetLike S M] (s : S) :
Function.Injective fun (a : s) => a
theorem AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_5 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedCancelAddCommMonoid M] [AddSubmonoidClass S M] (s : S) :
∀ (x : s) (x_1 : ), (x_1 x) = (x_1 x)
theorem AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_6 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedCancelAddCommMonoid M] (s : S) :
∀ (x x_1 : s), (x x_1) = (x x_1)
theorem AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_7 {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedCancelAddCommMonoid M] (s : S) :
∀ (x x_1 : s), (x x_1) = (x x_1)
theorem AddSubmonoid.toOrderedAddCommMonoid.proof_4 {M : Type u_1} [OrderedAddCommMonoid M] (S : AddSubmonoid M) :
∀ (x x_1 : S), (x + x_1) = (x + x_1)
theorem AddSubmonoid.toOrderedAddCommMonoid.proof_5 {M : Type u_1} [OrderedAddCommMonoid M] (S : AddSubmonoid M) :
∀ (x : S) (x_1 : ), (x_1 x) = (x_1 x)
theorem AddSubmonoid.toLinearOrderedAddCommMonoid.proof_5 {M : Type u_1} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) :
∀ (x : S) (x_1 : ), (x_1 x) = (x_1 x)
theorem AddSubmonoid.toLinearOrderedAddCommMonoid.proof_7 {M : Type u_1} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) :
∀ (x x_1 : S), (x x_1) = (x x_1)
theorem AddSubmonoid.toLinearOrderedAddCommMonoid.proof_4 {M : Type u_1} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) :
∀ (x x_1 : S), (x + x_1) = (x + x_1)
theorem AddSubmonoid.toLinearOrderedAddCommMonoid.proof_6 {M : Type u_1} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) :
∀ (x x_1 : S), (x x_1) = (x x_1)
theorem AddSubmonoid.toOrderedCancelAddCommMonoid.proof_4 {M : Type u_1} [OrderedCancelAddCommMonoid M] (S : AddSubmonoid M) :
∀ (x x_1 : S), (x + x_1) = (x + x_1)
theorem AddSubmonoid.toOrderedCancelAddCommMonoid.proof_5 {M : Type u_1} [OrderedCancelAddCommMonoid M] (S : AddSubmonoid M) :
∀ (x : S) (x_1 : ), (x_1 x) = (x_1 x)
theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_5 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) :
∀ (x : S) (x_1 : ), (x_1 x) = (x_1 x)
theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_4 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) :
∀ (x x_1 : S), (x + x_1) = (x + x_1)
theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_6 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) :
∀ (x x_1 : S), (x x_1) = (x x_1)
theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_7 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) :
∀ (x x_1 : S), (x x_1) = (x x_1)
theorem AddSubmonoid.nonneg.proof_1 (M : Type u_1) [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x x_1] :
∀ {a b : M}, 0 a0 b0 a + b
def AddSubmonoid.nonneg (M : Type u_1) [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x x_1] :

The submonoid of nonnegative elements.

Equations
Instances For
    @[simp]
    theorem Submonoid.oneLE_coe (M : Type u_1) [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x x_1] :
    @[simp]
    theorem AddSubmonoid.nonneg_coe (M : Type u_1) [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x x_1] :
    def Submonoid.oneLE (M : Type u_1) [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x x_1] :

    The submonoid of elements greater than 1.

    Equations
    Instances For
      @[simp]
      theorem AddSubmonoid.mem_nonneg {M : Type u_1} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x x_1] {a : M} :
      @[simp]
      theorem Submonoid.mem_oneLE {M : Type u_1} [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x x_1] {a : M} :

      The submonoid of positive elements.

      Equations
      Instances For
        @[simp]
        theorem Submonoid.mem_pos {α : Type u_2} [MulZeroOneClass α] [PartialOrder α] [PosMulStrictMono α] [ZeroLEOneClass α] [NeZero 1] {a : α} :