English
If α is AddCommMonoid, PartialOrder, IsOrderedAddMonoid and 0 ≤ a for all a, then WithZero α is an ordered AddMonoid.
Русский
Если α — аддитивный коммутативный моноид, частичный порядок и упорядоченный аддитивный моноид, и для всех a: 0 ≤ a, то WithZero α является упорядоченным аддитивным моноидом.
LaTeX
$$$[AddCommMonoid\ α] \land [PartialOrder\ α] \land [IsOrderedAddMonoid\ α] \land (\forall a, 0 \le a) \Rightarrow [IsOrderedAddMonoid(\mathrm{WithZero}\, α)]$$$
Lean4
/-- If `0` is the least element in `α`, then `WithZero α` is an ordered `AddMonoid`. -/
-- See note [reducible non-instances]
protected theorem isOrderedAddMonoid [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α]
(zero_le : ∀ a : α, 0 ≤ a) : IsOrderedAddMonoid (WithZero α) where
add_le_add_left := @add_le_add_left _ _ _ (WithZero.addLeftMono zero_le)
