Documentation

Mathlib.Algebra.Order.Monoid.Submonoid

Ordered instances on submonoids #

source
@[instance 75]
instance SubmonoidClass.toIsOrderedMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M] [SubmonoidClass S M] (s : S) :
IsOrderedMonoid ↥s

A submonoid of an ordered monoid is an ordered monoid.

source
@[instance 75]
instance AddSubmonoidClass.toIsOrderedAddMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] [AddSubmonoidClass S M] (s : S) :
IsOrderedAddMonoid ↥s

An AddSubmonoid of an ordered additive monoid is an ordered additive monoid.

source
@[instance 75]
instance SubmonoidClass.toIsOrderedCancelMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] [SubmonoidClass S M] (s : S) :
IsOrderedCancelMonoid ↥s

A submonoid of an ordered cancellative monoid is an ordered cancellative monoid.

source
@[instance 75]
instance AddSubmonoidClass.toIsOrderedCancelAddMonoid {M : Type u_1} {S : Type u_2} [SetLike S M] [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] [AddSubmonoidClass S M] (s : S) :
IsOrderedCancelAddMonoid ↥s

An AddSubmonoid of an ordered cancellative additive monoid is an ordered cancellative additive monoid.

source
instance Submonoid.toIsOrderedMonoid {M : Type u_1} [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M] (S : Submonoid M) :
IsOrderedMonoid ↥S

A submonoid of an ordered monoid is an ordered monoid.

source
instance AddSubmonoid.toIsOrderedAddMonoid {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] (S : AddSubmonoid M) :
IsOrderedAddMonoid ↥S

An AddSubmonoid of an ordered additive monoid is an ordered additive monoid.

source
instance Submonoid.toIsOrderedCancelMonoid {M : Type u_1} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] (S : Submonoid M) :
IsOrderedCancelMonoid ↥S

A submonoid of an ordered cancellative monoid is an ordered cancellative monoid.

source
instance AddSubmonoid.toIsOrderedCancelAddMonoid {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] (S : AddSubmonoid M) :
IsOrderedCancelAddMonoid ↥S

An AddSubmonoid of an ordered cancellative additive monoid is an ordered cancellative additive monoid.

source
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
Instances For
    source
    def AddSubmonoid.nonneg (M : Type u_1) [AddMonoid M] [Preorder M] [AddLeftMono M] :
    AddSubmonoid M

    The submonoid of nonnegative elements.

    Equations
    Instances For
      source
      @[simp]
      theorem AddSubmonoid.coe_nonneg (M : Type u_1) [AddMonoid M] [Preorder M] [AddLeftMono M] :
      ↑(nonneg M) = Set.Ici 0
      source
      @[simp]
      theorem Submonoid.coe_oneLE (M : Type u_1) [Monoid M] [Preorder M] [MulLeftMono M] :
      ↑(oneLE M) = Set.Ici 1
      source
      @[simp]
      theorem Submonoid.mem_oneLE {M : Type u_1} [Monoid M] [Preorder M] [MulLeftMono M] {a : M} :
      a ∈ oneLE M ↔ 1 ≤ a
      source
      @[simp]
      theorem AddSubmonoid.mem_nonneg {M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftMono M] {a : M} :
      a ∈ nonneg M ↔ 0 ≤ a