instFinitePolynomial — Mathlib

English

If M is a finite module over R, then AEval(R, M, a) is a finite module over the polynomial ring R[X].

Русский

Если M конечномерный модуль над R, то AEval(R, M, a) конечномерный модуль над кольцом многочленов R[X].

LaTeX

$$$\operatorname{Module\ Finite}(\operatorname{Polynomial} R)(\operatorname{AEval} R M a)$$$

Lean4

instance instFinitePolynomial [Module.Finite R M] : Module.Finite R[X] <| AEval R M a :=
  Finite.of_restrictScalars_finite R _ _

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