instNonAssocSemiring — Mathlib

English

WithTop α inherits a NonAssocSemiring structure whenever α has a NonAssocSemiring structure and suitable order properties.

Русский

WithTop α наследует структуру NonAssocSemiring, когда α обладает такой же структурой и соответствующим порядком.

LaTeX

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

Lean4

instance instNonAssocSemiring [NonAssocSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [Nontrivial α] :
    NonAssocSemiring (WithTop α)
    where
  toNonUnitalNonAssocSemiring := instNonUnitalNonAssocSemiring
  __ := WithTop.instMulZeroOneClass
  __ := WithTop.addCommMonoidWithOne

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