English
If α acts on K with a distributive action and IsScalarTower α K K holds, then α acts on the polynomial ring K[X] with a scalar-tower structure.
Русский
Если α действует на K с распределенным действием и выполняется IsScalarTower α K K, то α действует на полиномы над K[X] с башнеобразной структурой.
LaTeX
$$$\forall {\alpha K} [\mathrm{Semiring} K] [\mathrm{DistribSMul} \alpha K] [\mathrm{IsScalarTower} \alpha K K], \; \mathrm{IsScalarTower} \alpha (\mathrm{Polynomial} K) (\mathrm{Polynomial} K)$$$
Lean4
instance isScalarTower_right {α K : Type*} [Semiring K] [DistribSMul α K] [IsScalarTower α K K] :
IsScalarTower α K[X] K[X] :=
⟨by
rintro _ ⟨⟩ ⟨⟩
simp_rw [smul_eq_mul, ← ofFinsupp_smul, ← ofFinsupp_mul, ← ofFinsupp_smul, smul_mul_assoc]⟩
