Theorems · Theorem · linear algebra

LinearMap.aeval_eq_aeval_mod_charpoly

∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : Module.Finite R M] (f : M →ₗ[R] M) (p : Polynomial R),
  (Polynomial.aeval f) p = (Polynomial.aeval f) (p %ₘ f.charpoly)

Any endomorphism polynomial p is equivalent under evaluation to p %ₘ f.charpoly; that is, p is equivalent to a polynomial with degree less than the dimension of the module.

Defined in

Mathlib.LinearAlgebra.Charpoly.Basic

Cited by

1 results in Mathlib

Foundations

Depth 127 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModuleModule.FreeModule.Finite