instIsOrderedMonoid — Mathlib

English

If α is a commutative monoid with a partial order and the order is preserved under left-multiplication, then the opposite monoid αᵐᵒᵖ is also an IsOrderedMonoid.

Русский

Пусть α — коммутативный моноид с частичным порядком, удовлетворяющий условию моноидного упорядочения; тогда противоположный моноид αᵐᵒᵖ тоже является упорядоченным моноидом.

LaTeX

$$IsOrderedMonoid(αᵐᵒᵖ) given IsOrderedMonoid(α)$$

Lean4

@[to_additive]
instance [IsOrderedMonoid α] : IsOrderedMonoid αᵐᵒᵖ where
  mul_le_mul_left a b hab c := mul_le_mul_right' (by simpa) c.unop

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