English
The product of a family of canonically ordered monoids is canonically ordered.
Русский
Произведение семейства канонически упорядоченных моноидов также канонически упорядочено.
LaTeX
$$$\\prod_{i\\in I} Z_i\\text{ is canonically ordered given each } Z_i\\text{ is canonically ordered.}$$$
Lean4
/-- The product of a family of canonically ordered monoids is a canonically ordered monoid. -/
@[to_additive /-- The product of a family of canonically ordered additive monoids is
a canonically ordered additive monoid. -/
]
instance {ι : Type*} {Z : ι → Type*} [∀ i, Monoid (Z i)] [∀ i, PartialOrder (Z i)] [∀ i, CanonicallyOrderedMul (Z i)] :
CanonicallyOrderedMul (∀ i, Z i) where
__ := Pi.existsMulOfLe
le_mul_self _ _ := fun _ => le_mul_self
le_self_mul _ _ := fun _ => le_self_mul
