instCommSemiring — Mathlib

English

If α is a CommSemiring, then WithTop α is a CommSemiring as well.

Русский

Если α — коммутативное полугруппой кольцо (CommSemiring), то WithTop α тоже CommSemiring.

LaTeX

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

Lean4

instance instCommSemiring [CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [NoZeroDivisors α]
    [Nontrivial α] : CommSemiring (WithTop α)
    where
  toSemiring := WithTop.instSemiring
  __ := WithTop.instCommMonoidWithZero

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