isOrderedCancelMonoid — Mathlib

English

If each component f_i is an ordered cancellative monoid, then the product ∏_{i} f_i is an ordered cancellative monoid.

Русский

Если каждый компонент f_i является упорядоченным моноидом с свойством отмены, то их произведение является упорядоченным моноидом с отменой.

LaTeX

$$$\\prod_{i\\in I} f_i \\text{ is an ordered cancellative monoid (pointwise).}$$$

Lean4

@[to_additive]
instance isOrderedCancelMonoid [∀ i, CommMonoid <| f i] [∀ i, PartialOrder <| f i] [∀ i, IsOrderedCancelMonoid <| f i] :
    IsOrderedCancelMonoid (∀ i : I, f i) where le_of_mul_le_mul_left _ _ _ h i := le_of_mul_le_mul_left' (h i)

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