isOrderedCancelAddMonoid — Mathlib

English

If α is an ordered cancellative additive monoid, then the finsupp space ι →₀ α is an ordered cancellative additive monoid.

Русский

Если α — упорядоченный отменяемый аддитивный моноид, то ι →₀ α также является упорядоченным отменяемым аддитивным моноидом.

LaTeX

$$IsOrderedCancelAddMonoid (ι →₀ α)$$

Lean4

instance isOrderedCancelAddMonoid [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] :
    IsOrderedCancelAddMonoid (ι →₀ α) :=
  { le_of_add_le_add_left := fun _f _g _i h s => le_of_add_le_add_left (h s) }

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