English
If S acts distributively on R, then S acts distributively on the polynomial ring R[X].
Русский
Если S действует распределительно на R, то S действует распределительно на полиномы над R.
LaTeX
$$$\forall S\,[\mathrm{DistribSMul} S R]\Rightarrow \mathrm{DistribSMul} S (\mathrm{Polynomial} R)$$$
Lean4
instance distribSMul {S} [DistribSMul S R] : DistribSMul S R[X] :=
fast_instance%Function.Injective.distribSMul ⟨⟨toFinsupp, toFinsupp_zero⟩, toFinsupp_add⟩ toFinsupp_injective
toFinsupp_smul