isOrderedMonoid — Mathlib

English

If α has an additive commutative monoid structure with a compatible order and IsOrderedAddMonoid, then Multiplicative α is an ordered monoid.

Русский

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

LaTeX

$$IsOrderedMonoid(\mathrm{Multiplicative}(\alpha))$$

Lean4

instance isOrderedMonoid [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] :
    IsOrderedMonoid (Multiplicative α) :=
  { mul_le_mul_left := @IsOrderedAddMonoid.add_le_add_left α _ _ _ }

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