English
If S is a semiring and R is an S-module, then the polynomial ring R[X] is an S-module as well.
Русский
Если S — полусемиринг и R является модулем над S, то R[X] также является модулем над S.
LaTeX
$$$\forall S\,[\mathrm{Semiring} S] \to \mathrm{Module} S R[X]$$$
Lean4
instance module {S} [Semiring S] [Module S R] : Module S R[X] :=
fast_instance%Function.Injective.module _ ⟨⟨toFinsupp, toFinsupp_zero⟩, toFinsupp_add⟩ toFinsupp_injective
toFinsupp_smul