instCommSemiringOfCanonicallyOrderedAdd

English

If α is a commutative semiring with a partial order and canonically ordered addition, then NonemptyInterval(α) carries a commutative semiring structure (coordinatewise).

Русский

Если α является коммутативной полукольцом с частичной порядком и канонически упорядоченным добавлением, то NonemptyInterval(α) является коммутативной полукольцом (покомпонентно).

LaTeX

$$$[\mathrm{CommSemiring}(\alpha)]\land [\mathrm{PartialOrder}(\alpha)]\land [\mathrm{CanonicallyOrderedAdd}(\alpha)]\Rightarrow \mathrm{CommSemiring}(\mathrm{NonemptyInterval}(\alpha)).$$$

Lean4

instance [CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] : CommSemiring (NonemptyInterval α) :=
  NonemptyInterval.toProd_injective.commSemiring _ toProd_zero toProd_one toProd_add toProd_mul (swap toProd_nsmul)
    toProd_pow (fun _ => rfl)

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