instIsOrderedRing — Mathlib

English

WithTop α inherits IsOrderedRing when α is a CommSemiring with compatible order structure.

Русский

WithTop α имеет IsOrderedRing, если α — коммутативное кольцо с упорядочиванием и нужной структурой.

LaTeX

$$$\\\\mathrm{WithTop} \\alpha \\\\text{ is IsOrderedRing if } \\alpha \\\\text{ is}$$$

Lean4

instance instIsOrderedRing [CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [NoZeroDivisors α]
    [Nontrivial α] : IsOrderedRing (WithTop α) :=
  CanonicallyOrderedAdd.toIsOrderedRing

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