polynomialModule — Mathlib

English

The module PolynomialModule R M carries a canonical structure as a module over the polynomial ring R[X].

Русский

У модуля PolynomialModule R M есть естественная структура модуля над кольцом многочленов R[X].

LaTeX

$$$\text{Module}_{R[X]}(\text{PolynomialModule } R M)$$$

Lean4

noncomputable instance polynomialModule : Module R[X] (PolynomialModule R M) :=
  inferInstanceAs (Module R[X] (Module.AEval' (Finsupp.lmapDomain M R Nat.succ)))

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