isOrderedMonoid — Mathlib

English

If α is a commutative monoid with a compatible order (IsOrderedMonoid), then WithZero α is an ordered monoid, i.e., left-multiplication preserves order.

Русский

Если α — коммутативный моноид с совместимым порядком (IsOrderedMonoid), то WithZero α является упорядоченным моноидом: умножение слева сохраняет порядок.

LaTeX

$$$[CommMonoid\ α] \land [PartialOrder\ α] \land [IsOrderedMonoid\ α] :\; IsOrderedMonoid(\mathrm{WithZero}\, α)$$$

Lean4

instance isOrderedMonoid [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] : IsOrderedMonoid (WithZero α) where
  mul_le_mul_left := fun _ _ => mul_le_mul_left'

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