instCommSemiring — Mathlib

English

If Γ is an additive ordered monoid and R is a semiring, then HahnSeries(Γ,R) forms a commutative semiring.

Русский

Пусть Γ имеет структуру упорядоченного добавочного моноида и R — полукольцо; тогда HahnSeries(Γ,R) образует коммутативную полукольцо.

LaTeX

$$$\\text{HahnSeries}(\\Gamma,R) \\text{ is a commutative semiring}$$$

Lean4

instance [CommSemiring R] : CommSemiring (HahnSeries Γ R) :=
  { inferInstanceAs (NonUnitalCommSemiring (HahnSeries Γ R)), inferInstanceAs (Semiring (HahnSeries Γ R)) with }

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