instSemiring — Mathlib

English

If α is a Semiring with the usual order conditions, then WithTop α is a Semiring.

Русский

Если α является полугруппой полукольцом (Semiring) с обычным порядком, то WithTop α — тоже Semiring.

LaTeX

$$$\\\\mathrm{WithTop} \\alpha \\\\text{ is a Semiring if } \\alpha \\\\text{ is}$$$

Lean4

instance instSemiring [Semiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [NoZeroDivisors α] [Nontrivial α] :
    Semiring (WithTop α) where
  toNonUnitalSemiring := WithTop.instNonUnitalSemiring
  __ := WithTop.instMonoidWithZero
  __ := WithTop.addCommMonoidWithOne

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