Documentation

Mathlib.Algebra.Order.Monoid.Submonoid

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] :

The submonoid of elements that are at least 1.

Equations

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

Instances For

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

The submonoid of nonnegative elements.

Equations

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

Instances For

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