English
If α is a commutative semiring with order and IsOrderedRing, CanonicallyOrderedAdd, NoZeroDivisors, and Nontrivial, then WithBot α is an IsOrderedRing; the order-structural laws extend from α.
Русский
Если α — упорядоченное коммутативное полукольцо с IsOrderedRing, CanonicallyOrderedAdd, NoZeroDivisors и ненулевым, то WithBot α является упорядоченным кольцом; законы порядка переходят из α.
LaTeX
$$$\text{WithBot } α \text{ is IsOrderedRing}$ under the given conditions on α$$
Lean4
instance instIsOrderedRing [CommSemiring α] [PartialOrder α] [IsOrderedRing α] [CanonicallyOrderedAdd α]
[NoZeroDivisors α] [Nontrivial α] : IsOrderedRing (WithBot α)
where
mul_le_mul_of_nonneg_left _ _ _ := mul_le_mul_of_nonneg_left
mul_le_mul_of_nonneg_right _ _ _ := mul_le_mul_of_nonneg_right
