distribMulAction — Mathlib

English

If S is a Monoid acting on R with a distributive action, then S acts on the polynomial ring R[X] by a compatible action.

Русский

Если S является моноидом, действующим расрпределительно на R, то S действует на R[X] совместно, образуя распределенное действие умножения.

LaTeX

$$$\forall S\,[\mathrm{Monoid}\, S] \,[\mathrm{DistribMulAction} S R] \Rightarrow \mathrm{DistribMulAction} S (\mathrm{Polynomial} R)$$$

Lean4

instance distribMulAction {S} [Monoid S] [DistribMulAction S R] : DistribMulAction S R[X] :=
  fast_instance%Function.Injective.distribMulAction ⟨⟨toFinsupp, toFinsupp_zero (R := R)⟩, toFinsupp_add⟩
      toFinsupp_injective toFinsupp_smul

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