module — Mathlib

English

If S is a semiring and R is an S-module, then the polynomial ring R[X] is an S-module as well.

Русский

Если S — полусемиринг и R является модулем над S, то R[X] также является модулем над S.

LaTeX

$$$\forall S\,[\mathrm{Semiring} S] \to \mathrm{Module} S R[X]$$$

Lean4

instance module {S} [Semiring S] [Module S R] : Module S R[X] :=
  fast_instance%Function.Injective.module _ ⟨⟨toFinsupp, toFinsupp_zero⟩, toFinsupp_add⟩ toFinsupp_injective
      toFinsupp_smul

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