English
MvPowerSeries σ R forms a semiring when R is a semiring; the operations are defined by the usual convolution formulas.
Русский
MvPowerSeries σ R образует полупрямое полугрупповое кольцо, когда R — полукольцо; операции заданы свёрткой.
LaTeX
$$$$ \, ext{Semiring} \bigl( \mathrm{MvPowerSeries}(σ,R) \bigr) $$$$
Lean4
instance : Semiring (MvPowerSeries σ R) :=
{ inferInstanceAs (AddMonoidWithOne (MvPowerSeries σ R)), inferInstanceAs (Mul (MvPowerSeries σ R)),
inferInstanceAs (AddCommMonoid
(MvPowerSeries σ R)) with
mul_one := MvPowerSeries.mul_one
one_mul := MvPowerSeries.one_mul
mul_assoc := MvPowerSeries.mul_assoc
mul_zero := MvPowerSeries.mul_zero
zero_mul := MvPowerSeries.zero_mul
left_distrib := MvPowerSeries.mul_add
right_distrib := MvPowerSeries.add_mul }
