toIsOrderedCancelMonoid — Mathlib

English

A submonoid S of an ordered cancellative monoid M is an IsOrderedCancelMonoid.

Русский

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

LaTeX

$$IsOrderedCancelMonoid S$$

Lean4

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

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