English
If α is an AddMonoid with a PartialOrder and CanonicallyOrderedAdd, then Multiplicative α is CanonicallyOrderedMul, i.e., left and right multiplications preserve and reflect the order in the canonical sense.
Русский
Пусть α — аддитивный моноид с частичным порядком и CanonicallyOrderedAdd; тогда Multiplicative α — канонически упорядоченный моноид с умножением, т.е. левые и правые умножения сохраняют порядок в каноническом смысле.
LaTeX
$$$[\text{AddMonoid}(\alpha)]\,[\text{PartialOrder}(\alpha)]\,[\text{CanonicallyOrderedAdd}(\alpha)] \Rightarrow \text{CanonicallyOrderedMul}(\mathrm{Multiplicative}(\alpha)).$$$
Lean4
instance canonicallyOrderedMul [AddMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] :
CanonicallyOrderedMul (Multiplicative α)
where
le_mul_self _ _ := le_add_self (α := α)
le_self_mul _ _ := le_self_add (α := α)
