isOrderedCancelMonoid — Mathlib

English

The Lex product Lex(α, β) is an IsOrderedCancelMonoid when α and β are appropriately structured.

Русский

Лексикографическое произведение Lex(α, β) является упорядоченным отменяемым моноидом при надлежащей структуре α и β.

LaTeX

$$IsOrderedCancelMonoid(Lex(α, β))$$

Lean4

@[to_additive]
instance isOrderedCancelMonoid [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] [CommMonoid β] [PartialOrder β]
    [IsOrderedCancelMonoid β] : IsOrderedCancelMonoid (α ×ₗ β)
    where
  mul_le_mul_left _ _ := mul_le_mul_left'
  le_of_mul_le_mul_left _ _ _
    hxyz :=
    (le_iff.1 hxyz).elim (fun hxy => left _ _ <| lt_of_mul_lt_mul_left' hxy)
      (fun hxy => le_iff.2 <| Or.inr ⟨mul_left_cancel hxy.1, le_of_mul_le_mul_left' hxy.2⟩)

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