Polynomial modules in finite dimensions

This file is a place to collect results about the R[X]-module structure induced on an R-module by an R-linear endomorphism, which require the concept of finite-dimensionality.

Main results:

• Module.AEval.isTorsion_of_finiteDimensional: if a vector space M with coefficients in a field K carries a natural K-linear endomorphism which belongs to a finite-dimensional algebra over K, then the induced K[X]-module structure on M is pure torsion.

theorem Module.AEval.isTorsion_of_aeval_eq_zero {R : Type u_1} {M : Type u_3} {A : Type u_4} {a : A} [CommSemiring R] [NoZeroDivisors R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] {p : Polynomial R} (h : (Polynomial.aeval a) p = 0) (h' : p ≠ 0) : Module.IsTorsion (Polynomial R) (Module.AEval R M a)

theorem Module.AEval.isTorsion_of_finiteDimensional (K : Type u_2) (M : Type u_3) {A : Type u_4} (a : A) [Field K] [Ring A] [Algebra K A] [AddCommGroup M] [Module A M] [Module K M] [IsScalarTower K A M] [FiniteDimensional K A] : Module.IsTorsion (Polynomial K) (Module.AEval K M a)