Commit 2023-11-01 17:24 0e345e85

feat(Data/Polynomial/Module) : define an R[X] module, given a linear map. (#7728) Given an element a in an R-algebra A and an A-module M, define an R[X]-module Module.AEval R M a, whose elements correspond to elements of M, and where the action of f : R[X] is f • m = aeval a f • m. Equivalently, X • m = a • m. This module is abbreviated to Module.AEval' φ in the special case that A is the algebra of R-linear maps and φ : M → M is an R-linear map. This is needed in #7419.