instIsOrderedCancelMonoid — Mathlib

English

If α and β are ordered cancellative monoids, their product α × β is an ordered cancellative monoid.

Русский

Если α и β — упорядоченные отменяемые моноиды, то их произведение α × β является упорядоченным отменяемым моноидом.

LaTeX

$$IsOrderedCancelMonoid(α × β)$$

Lean4

@[to_additive]
instance instIsOrderedCancelMonoid [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] [CommMonoid β]
    [PartialOrder β] [IsOrderedCancelMonoid β] : IsOrderedCancelMonoid (α × β) :=
  { le_of_mul_le_mul_left := fun _ _ _ h ↦ ⟨le_of_mul_le_mul_left' h.1, le_of_mul_le_mul_left' h.2⟩ }

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