instIdemSemiringOfMonoid — Mathlib

English

There is a canonical IdemSemiring structure on SetSemiring α when α is a Monoid.

Русский

Если α является моноидом, то SetSemiring α естественным образом является IdemSemiring.

LaTeX

$$IdemSemiring (SetSemiring α)$$

Lean4

noncomputable instance [Monoid α] : IdemSemiring (SetSemiring α) :=
  { (inferInstance : NonAssocSemiring (SetSemiring α)), (inferInstance : NonUnitalSemiring (SetSemiring α)),
    (inferInstance : CompleteBooleanAlgebra (Set α)) with }

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