Documentation

Mathlib.Data.Polynomial.Module.FiniteDimensional

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: #

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) :
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] :