instIsOrderedRing — Mathlib

English

If α is a commutative monoid, then the collection of all subsets of α, with union as addition and setwise product as multiplication, forms an ordered ring under inclusion.

Русский

Пусть α — коммутативный моноид. Тогда множество всех подмножеств α, со сложением даваемым как объединение и умножением — как произведение множеств, образует упорядоченное кольцо под включением.

LaTeX

$$$\\text{If } (\\alpha,\\cdot,1) \\text{ is a commutative monoid, then } (\\mathcal{P}(\\alpha), \\cup, \\cdot, \\emptyset) \\text{ is an ordered ring.}$$$

Lean4

noncomputable instance [CommMonoid α] : IsOrderedRing (SetSemiring α) :=
  CanonicallyOrderedAdd.toIsOrderedRing

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