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 = OrderedCommMonoid.mk ⋯

@[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 = OrderedAddCommMonoid.mk ⋯

@[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 = LinearOrderedCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

@[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 = LinearOrderedAddCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

@[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 = OrderedCancelCommMonoid.mk ⋯

@[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 = OrderedCancelAddCommMonoid.mk ⋯

@[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

• One or more equations did not get rendered due to their size.

@[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

• One or more equations did not get rendered due to their size.

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 = SubmonoidClass.toOrderedCommMonoid S

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 = AddSubmonoidClass.toOrderedAddCommMonoid S

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 = SubmonoidClass.toLinearOrderedCommMonoid S

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 = AddSubmonoidClass.toLinearOrderedAddCommMonoid S

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 = SubmonoidClass.toOrderedCancelCommMonoid S

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 = AddSubmonoidClass.toOrderedCancelAddCommMonoid S

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 = SubmonoidClass.toLinearOrderedCancelCommMonoid S

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 = AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid S

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

The submonoid of elements that are at least 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.coe_oneLE (M : Type u_1) [Monoid M] [Preorder M] [MulLeftMono M] : ↑(oneLE M) = Set.Ici 1

@[simp]

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

@[simp]

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

@[simp]

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