isOrderedCancelAddMonoid — Mathlib

English

If α is a commutative monoid with a partial order and IsOrderedCancelMonoid, then Additive α is an IsOrderedCancelAddMonoid.

Русский

Если α — коммутативный моноид с частичным порядком и IsOrderedMonoid, тогда Additive α — упорядоченный отменяемый аддитивный моноид.

LaTeX

$$$[\text{CommMonoid}(\alpha)]\,[\text{PartialOrder}(\alpha)]\,[\text{IsOrderedMonoid}(\alpha)] \Rightarrow \text{IsOrderedCancelAddMonoid}(\mathrm{Additive}(\alpha)).$$$

Lean4

instance isOrderedCancelAddMonoid [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] :
    IsOrderedCancelAddMonoid (Additive α) :=
  { le_of_add_le_add_left := @IsOrderedCancelMonoid.le_of_mul_le_mul_left α _ _ _ }

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