instNonUnitalSemiring — Mathlib

English

WithTop α inherits a NonUnitalSemiring structure from α under the given order assumptions.

Русский

WithTop α наследует структуру NonUnitalSemiring от α при заданных условиях порядка.

LaTeX

$$$\\\\mathrm{WithTop} \\\\alpha \\\\text{ is a NonUnitalSemiring}$$$

Lean4

instance instNonUnitalSemiring [NonUnitalSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [NoZeroDivisors α] :
    NonUnitalSemiring (WithTop α)
    where
  toNonUnitalNonAssocSemiring := WithTop.instNonUnitalNonAssocSemiring
  __ := WithTop.instSemigroupWithZero

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