distribSMul — Mathlib

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

Похожие утверждения