English
There is a natural extension of a MulSemiringAction from a base ring R to the polynomial ring R[X], turning polynomials into a MulSemiringAction themselves, compatible with smul_one and smul_mul.
Русский
Существует естественное продолжение действия MulSemiringAction с оснорвого кольца R на кольцо многочленов R[X], сохраняющее структуру: smul_one и smul_mul выполняются для многочленов.
LaTeX
$$$\text{instance } [MulSemiringAction M R] \Rightarrow [MulSemiringAction M (R[X])]$ with smul_one and smul_mul as specified.$$
Lean4
noncomputable instance [MulSemiringAction M R] : MulSemiringAction M R[X] :=
{
Polynomial.distribMulAction with
smul_one := fun m ↦ smul_eq_map R m ▸ Polynomial.map_one (MulSemiringAction.toRingHom M R m)
smul_mul := fun m _ _ ↦ smul_eq_map R m ▸ Polynomial.map_mul (MulSemiringAction.toRingHom M R m) }
