toIsOrderedCancelMonoid — Mathlib

English

A Submonoid S of an ordered cancellative monoid is an IsOrderedCancelMonoid.

Русский

Подмножество S упорядоченного отменяемого моноида является IsOrderedCancelMonoid.

LaTeX

$$IsOrderedCancelMonoid (Subtype fun x => x ∈ S)$$

Lean4

/-- A submonoid of an ordered cancellative monoid is an ordered cancellative monoid. -/
@[to_additive AddSubmonoid.toIsOrderedCancelAddMonoid /--
    An `AddSubmonoid` of an ordered cancellative additive monoid is an ordered cancellative
          additive monoid. -/
    ]
instance toIsOrderedCancelMonoid [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] (S : Submonoid M) :
    IsOrderedCancelMonoid S :=
  Function.Injective.isOrderedCancelMonoid Subtype.val (fun _ _ => rfl) .rfl

Похожие утверждения