isOrderedCancelMonoid — Mathlib

English

If α is an AddCommMonoid with a PartialOrder and IsOrderedCancelAddMonoid, then the multiplicative structure on α is an IsOrderedCancelMonoid.

Русский

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

LaTeX

$$$[\text{AddCommMonoid}(\alpha)]\,[\text{PartialOrder}(\alpha)]\,[\text{IsOrderedCancelAddMonoid}(\alpha)] \Rightarrow \text{IsOrderedCancelMonoid}(\mathrm{Multiplicative}(\alpha)).$$$

Lean4

instance isOrderedCancelMonoid [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] :
    IsOrderedCancelMonoid (Multiplicative α) :=
  { le_of_mul_le_mul_left := @IsOrderedCancelAddMonoid.le_of_add_le_add_left α _ _ _ }

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