isOrderedCancelMonoid — Mathlib

English

If α is an ordered cancellative monoid, then its order dual αᵒᵈ is an IsOrderedCancelMonoid.

Русский

Если α — упорядоченный отменяемый моноид, то αᵒᵈ по порядку тоже является упорядоченным отменяемым моноидом.

LaTeX

$$IsOrderedCancelMonoid(α^{\mathrm{op}})$$

Lean4

@[to_additive]
instance isOrderedCancelMonoid [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] : IsOrderedCancelMonoid αᵒᵈ :=
  { le_of_mul_le_mul_left := fun _ _ _ : α => le_of_mul_le_mul_left' }

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