instCanonicallyOrderedMul — Mathlib

English

The product α × β of canonically ordered monoids is canonically ordered.

Русский

Произведение канонически упорядоченных моноидов α × β является канонически упорядоченным моноидом.

LaTeX

$$CanonicallyOrderedMul(α × β)$$

Lean4

@[to_additive]
instance [Mul α] [LE α] [CanonicallyOrderedMul α] [Mul β] [LE β] [CanonicallyOrderedMul β] :
    CanonicallyOrderedMul (α × β)
    where
  le_mul_self := fun _ _ ↦ le_def.mpr ⟨le_mul_self, le_mul_self⟩
  le_self_mul := fun _ _ ↦ le_def.mpr ⟨le_self_mul, le_self_mul⟩

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