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 Submonoid.coe_oneLE (M : Type u_1) [Monoid M] [Preorder M] [MulLeftMono M] :
          ↑(oneLE M) = Set.Ici 1
          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.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