Ordered instances on submonoids

@[instance 75]

instance SubmonoidClass.toOrderedCommMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedCommMonoid M] [SubmonoidClass S M] (s : S) : OrderedCommMonoid ↥s

A submonoid of an OrderedCommMonoid is an OrderedCommMonoid.

Equations

• SubmonoidClass.toOrderedCommMonoid s = Function.Injective.orderedCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

@[instance 75]

instance AddSubmonoidClass.toOrderedAddCommMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : OrderedAddCommMonoid ↥s

An AddSubmonoid of an OrderedAddCommMonoid is an OrderedAddCommMonoid.

Equations

• AddSubmonoidClass.toOrderedAddCommMonoid s = Function.Injective.orderedAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

@[instance 75]

instance SubmonoidClass.toLinearOrderedCommMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedCommMonoid M] [SubmonoidClass S M] (s : S) : LinearOrderedCommMonoid ↥s

A submonoid of a LinearOrderedCommMonoid is a LinearOrderedCommMonoid.

Equations

• SubmonoidClass.toLinearOrderedCommMonoid s = Function.Injective.linearOrderedCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance 75]

instance AddSubmonoidClass.toLinearOrderedAddCommMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : LinearOrderedAddCommMonoid ↥s

An AddSubmonoid of a LinearOrderedAddCommMonoid is a LinearOrderedAddCommMonoid.

Equations

• AddSubmonoidClass.toLinearOrderedAddCommMonoid s = Function.Injective.linearOrderedAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance 75]

instance SubmonoidClass.toOrderedCancelCommMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedCancelCommMonoid M] [SubmonoidClass S M] (s : S) : OrderedCancelCommMonoid ↥s

A submonoid of an OrderedCancelCommMonoid is an OrderedCancelCommMonoid.

Equations

• SubmonoidClass.toOrderedCancelCommMonoid s = Function.Injective.orderedCancelCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

@[instance 75]

instance AddSubmonoidClass.toOrderedCancelAddCommMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [OrderedCancelAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : OrderedCancelAddCommMonoid ↥s

An AddSubmonoid of an OrderedCancelAddCommMonoid is an OrderedCancelAddCommMonoid.

Equations

• AddSubmonoidClass.toOrderedCancelAddCommMonoid s = Function.Injective.orderedCancelAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

@[instance 75]

instance SubmonoidClass.toLinearOrderedCancelCommMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedCancelCommMonoid M] [SubmonoidClass S M] (s : S) : LinearOrderedCancelCommMonoid ↥s

A submonoid of a LinearOrderedCancelCommMonoid is a LinearOrderedCancelCommMonoid.

Equations

• SubmonoidClass.toLinearOrderedCancelCommMonoid s = Function.Injective.linearOrderedCancelCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance 75]

instance AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [LinearOrderedCancelAddCommMonoid M] [AddSubmonoidClass S M] (s : S) : LinearOrderedCancelAddCommMonoid ↥s

An AddSubmonoid of a LinearOrderedCancelAddCommMonoid is a LinearOrderedCancelAddCommMonoid.

Equations

• AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid s = Function.Injective.linearOrderedCancelAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance Submonoid.toOrderedCommMonoid {M : Type u_1} [OrderedCommMonoid M] (S : Submonoid M) : OrderedCommMonoid ↥S

A submonoid of an OrderedCommMonoid is an OrderedCommMonoid.

Equations

• S.toOrderedCommMonoid = Function.Injective.orderedCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

instance AddSubmonoid.toOrderedAddCommMonoid {M : Type u_1} [OrderedAddCommMonoid M] (S : AddSubmonoid M) : OrderedAddCommMonoid ↥S

An AddSubmonoid of an OrderedAddCommMonoid is an OrderedAddCommMonoid.

Equations

• S.toOrderedAddCommMonoid = Function.Injective.orderedAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

instance Submonoid.toLinearOrderedCommMonoid {M : Type u_1} [LinearOrderedCommMonoid M] (S : Submonoid M) : LinearOrderedCommMonoid ↥S

A submonoid of a LinearOrderedCommMonoid is a LinearOrderedCommMonoid.

Equations

• S.toLinearOrderedCommMonoid = Function.Injective.linearOrderedCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance AddSubmonoid.toLinearOrderedAddCommMonoid {M : Type u_1} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) : LinearOrderedAddCommMonoid ↥S

An AddSubmonoid of a LinearOrderedAddCommMonoid is a LinearOrderedAddCommMonoid.

Equations

• S.toLinearOrderedAddCommMonoid = Function.Injective.linearOrderedAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance Submonoid.toOrderedCancelCommMonoid {M : Type u_1} [OrderedCancelCommMonoid M] (S : Submonoid M) : OrderedCancelCommMonoid ↥S

A submonoid of an OrderedCancelCommMonoid is an OrderedCancelCommMonoid.

Equations

• S.toOrderedCancelCommMonoid = Function.Injective.orderedCancelCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

instance AddSubmonoid.toOrderedCancelAddCommMonoid {M : Type u_1} [OrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : OrderedCancelAddCommMonoid ↥S

An AddSubmonoid of an OrderedCancelAddCommMonoid is an OrderedCancelAddCommMonoid.

Equations

• S.toOrderedCancelAddCommMonoid = Function.Injective.orderedCancelAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

instance Submonoid.toLinearOrderedCancelCommMonoid {M : Type u_1} [LinearOrderedCancelCommMonoid M] (S : Submonoid M) : LinearOrderedCancelCommMonoid ↥S

A submonoid of a LinearOrderedCancelCommMonoid is a LinearOrderedCancelCommMonoid.

Equations

• S.toLinearOrderedCancelCommMonoid = Function.Injective.linearOrderedCancelCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance AddSubmonoid.toLinearOrderedCancelAddCommMonoid {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : LinearOrderedCancelAddCommMonoid ↥S

An AddSubmonoid of a LinearOrderedCancelAddCommMonoid is a LinearOrderedCancelAddCommMonoid.

Equations

• S.toLinearOrderedCancelAddCommMonoid = Function.Injective.linearOrderedCancelAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def Submonoid.oneLE (M : Type u_1) [Monoid M] [Preorder M] [MulLeftMono M] : Submonoid M

The submonoid of elements greater than 1.

Equations

• Submonoid.oneLE M = { carrier := Set.Ici 1, mul_mem' := ⋯, one_mem' := ⋯ }

def AddSubmonoid.nonneg (M : Type u_1) [AddMonoid M] [Preorder M] [AddLeftMono M] : AddSubmonoid M

The submonoid of nonnegative elements.

Equations

• AddSubmonoid.nonneg M = { carrier := Set.Ici 0, add_mem' := ⋯, zero_mem' := ⋯ }

@[simp]

theorem Submonoid.oneLE_coe (M : Type u_1) [Monoid M] [Preorder M] [MulLeftMono M] : ↑(Submonoid.oneLE M) = Set.Ici 1

@[simp]

theorem AddSubmonoid.nonneg_coe (M : Type u_1) [AddMonoid M] [Preorder M] [AddLeftMono M] : ↑(AddSubmonoid.nonneg M) = Set.Ici 0

@[simp]

theorem Submonoid.mem_oneLE {M : Type u_1} [Monoid M] [Preorder M] [MulLeftMono M] {a : M} : a ∈ Submonoid.oneLE M ↔ 1 ≤ a

@[simp]

theorem AddSubmonoid.mem_nonneg {M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftMono M] {a : M} : a ∈ AddSubmonoid.nonneg M ↔ 0 ≤ a